(0) Obligation:

Clauses:

eq(t, t).
eq(f, f).
neq(t, f).
neq(f, t).
del(X1, [], []).
del(X, .(Y, YS), YS) :- eq(X, Y).
del(X, .(Y, YS), .(Y, ZS)) :- ','(neq(X, Y), del(X, YS, ZS)).
ge(t, t).
ge(t, f).
ge(f, f).
gt(t, f).
max([], f).
max(.(X, []), X).
max(.(X, .(Y, XS)), Z) :- ','(ge(X, Y), max(.(X, XS), Z)).
max(.(X, .(Y, XS)), Z) :- ','(gt(Y, X), max(.(Y, XS), Z)).
maxsort([], []).
maxsort(.(X, XS), .(Y, YS)) :- ','(max(.(X, XS), Y), ','(del(Y, .(X, XS), ZS), maxsort(ZS, YS))).

Query: maxsort(g,a)

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph DT10.

(2) Obligation:

Triples:

maxC(.(t, X1), X2) :- maxC(X1, X2).
maxC(.(f, X1), X2) :- maxC(X1, X2).
delI(.(t, X1), .(t, X2)) :- delI(X1, X2).
maxF(.(f, X1), X2) :- maxF(X1, X2).
maxF(.(t, X1), X2) :- maxC(X1, X2).
delJ(.(f, X1), .(f, X2)) :- delJ(X1, X2).
maxsortA(.(X1, []), .(X1, X2)) :- ','(delcB(X1, X3), maxsortA(X3, X2)).
maxsortA(.(t, .(t, X1)), .(X2, X3)) :- maxC(X1, X2).
maxsortA(.(t, .(t, X1)), .(f, X2)) :- ','(maxcC(X1, f), delI(X1, X3)).
maxsortA(.(t, .(t, X1)), .(X2, X3)) :- ','(maxcC(X1, X2), ','(delcD(X2, X1, X4), maxsortA(X4, X3))).
maxsortA(.(t, .(f, X1)), .(X2, X3)) :- maxC(X1, X2).
maxsortA(.(t, .(f, X1)), .(f, X2)) :- ','(maxcC(X1, f), delI(.(f, X1), X3)).
maxsortA(.(t, .(f, X1)), .(X2, X3)) :- ','(maxcC(X1, X2), ','(delcE(X2, X1, X4), maxsortA(X4, X3))).
maxsortA(.(f, .(f, X1)), .(X2, X3)) :- maxF(X1, X2).
maxsortA(.(f, .(f, X1)), .(t, X2)) :- ','(maxcF(X1, t), delJ(X1, X3)).
maxsortA(.(f, .(f, X1)), .(X2, X3)) :- ','(maxcF(X1, X2), ','(delcG(X2, X1, X4), maxsortA(X4, X3))).
maxsortA(.(f, .(t, X1)), .(X2, X3)) :- maxC(X1, X2).
maxsortA(.(f, .(t, X1)), .(t, X2)) :- ','(maxcC(X1, t), delJ(.(t, X1), X3)).
maxsortA(.(f, .(t, X1)), .(X2, X3)) :- ','(maxcC(X1, X2), ','(delcH(X2, X1, X4), maxsortA(X4, X3))).

Clauses:

maxsortcA([], []).
maxsortcA(.(X1, []), .(X1, X2)) :- ','(delcB(X1, X3), maxsortcA(X3, X2)).
maxsortcA(.(t, .(t, X1)), .(X2, X3)) :- ','(maxcC(X1, X2), ','(delcD(X2, X1, X4), maxsortcA(X4, X3))).
maxsortcA(.(t, .(f, X1)), .(X2, X3)) :- ','(maxcC(X1, X2), ','(delcE(X2, X1, X4), maxsortcA(X4, X3))).
maxsortcA(.(f, .(f, X1)), .(X2, X3)) :- ','(maxcF(X1, X2), ','(delcG(X2, X1, X4), maxsortcA(X4, X3))).
maxsortcA(.(f, .(t, X1)), .(X2, X3)) :- ','(maxcC(X1, X2), ','(delcH(X2, X1, X4), maxsortcA(X4, X3))).
maxcC([], t).
maxcC(.(t, X1), X2) :- maxcC(X1, X2).
maxcC(.(f, X1), X2) :- maxcC(X1, X2).
delcI([], []).
delcI(.(f, X1), X1).
delcI(.(t, X1), .(t, X2)) :- delcI(X1, X2).
maxcF([], f).
maxcF(.(f, X1), X2) :- maxcF(X1, X2).
maxcF(.(t, X1), X2) :- maxcC(X1, X2).
delcJ([], []).
delcJ(.(t, X1), X1).
delcJ(.(f, X1), .(f, X2)) :- delcJ(X1, X2).
delcB(t, []).
delcB(f, []).
delcD(t, X1, .(t, X1)).
delcD(f, X1, .(t, .(t, X2))) :- delcI(X1, X2).
delcE(t, X1, .(f, X1)).
delcE(f, X1, .(t, X2)) :- delcI(.(f, X1), X2).
delcG(f, X1, .(f, X1)).
delcG(t, X1, .(f, .(f, X2))) :- delcJ(X1, X2).
delcH(f, X1, .(t, X1)).
delcH(t, X1, .(f, X2)) :- delcJ(.(t, X1), X2).

Afs:

maxsortA(x1, x2)  =  maxsortA(x1)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
maxsortA_in: (b,f)
maxC_in: (b,f)
maxcC_in: (b,b) (b,f)
delI_in: (b,f)
delcD_in: (b,b,f)
delcI_in: (b,f)
delcE_in: (b,b,f)
maxF_in: (b,f)
maxcF_in: (b,b) (b,f)
delJ_in: (b,f)
delcG_in: (b,b,f)
delcJ_in: (b,f)
delcH_in: (b,b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

MAXSORTA_IN_GA(.(X1, []), .(X1, X2)) → U7_GA(X1, X2, delcB_in_ga(X1, X3))
U7_GA(X1, X2, delcB_out_ga(X1, X3)) → U8_GA(X1, X2, maxsortA_in_ga(X3, X2))
U7_GA(X1, X2, delcB_out_ga(X1, X3)) → MAXSORTA_IN_GA(X3, X2)
MAXSORTA_IN_GA(.(t, .(t, X1)), .(X2, X3)) → U9_GA(X1, X2, X3, maxC_in_ga(X1, X2))
MAXSORTA_IN_GA(.(t, .(t, X1)), .(X2, X3)) → MAXC_IN_GA(X1, X2)
MAXC_IN_GA(.(t, X1), X2) → U1_GA(X1, X2, maxC_in_ga(X1, X2))
MAXC_IN_GA(.(t, X1), X2) → MAXC_IN_GA(X1, X2)
MAXC_IN_GA(.(f, X1), X2) → U2_GA(X1, X2, maxC_in_ga(X1, X2))
MAXC_IN_GA(.(f, X1), X2) → MAXC_IN_GA(X1, X2)
MAXSORTA_IN_GA(.(t, .(t, X1)), .(f, X2)) → U10_GA(X1, X2, maxcC_in_gg(X1, f))
U10_GA(X1, X2, maxcC_out_gg(X1, f)) → U11_GA(X1, X2, delI_in_ga(X1, X3))
U10_GA(X1, X2, maxcC_out_gg(X1, f)) → DELI_IN_GA(X1, X3)
DELI_IN_GA(.(t, X1), .(t, X2)) → U3_GA(X1, X2, delI_in_ga(X1, X2))
DELI_IN_GA(.(t, X1), .(t, X2)) → DELI_IN_GA(X1, X2)
MAXSORTA_IN_GA(.(t, .(t, X1)), .(X2, X3)) → U12_GA(X1, X2, X3, maxcC_in_ga(X1, X2))
U12_GA(X1, X2, X3, maxcC_out_ga(X1, X2)) → U13_GA(X1, X2, X3, delcD_in_gga(X2, X1, X4))
U13_GA(X1, X2, X3, delcD_out_gga(X2, X1, X4)) → U14_GA(X1, X2, X3, maxsortA_in_ga(X4, X3))
U13_GA(X1, X2, X3, delcD_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4, X3)
MAXSORTA_IN_GA(.(t, .(f, X1)), .(X2, X3)) → U15_GA(X1, X2, X3, maxC_in_ga(X1, X2))
MAXSORTA_IN_GA(.(t, .(f, X1)), .(X2, X3)) → MAXC_IN_GA(X1, X2)
MAXSORTA_IN_GA(.(t, .(f, X1)), .(f, X2)) → U16_GA(X1, X2, maxcC_in_gg(X1, f))
U16_GA(X1, X2, maxcC_out_gg(X1, f)) → U17_GA(X1, X2, delI_in_ga(.(f, X1), X3))
U16_GA(X1, X2, maxcC_out_gg(X1, f)) → DELI_IN_GA(.(f, X1), X3)
MAXSORTA_IN_GA(.(t, .(f, X1)), .(X2, X3)) → U18_GA(X1, X2, X3, maxcC_in_ga(X1, X2))
U18_GA(X1, X2, X3, maxcC_out_ga(X1, X2)) → U19_GA(X1, X2, X3, delcE_in_gga(X2, X1, X4))
U19_GA(X1, X2, X3, delcE_out_gga(X2, X1, X4)) → U20_GA(X1, X2, X3, maxsortA_in_ga(X4, X3))
U19_GA(X1, X2, X3, delcE_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4, X3)
MAXSORTA_IN_GA(.(f, .(f, X1)), .(X2, X3)) → U21_GA(X1, X2, X3, maxF_in_ga(X1, X2))
MAXSORTA_IN_GA(.(f, .(f, X1)), .(X2, X3)) → MAXF_IN_GA(X1, X2)
MAXF_IN_GA(.(f, X1), X2) → U4_GA(X1, X2, maxF_in_ga(X1, X2))
MAXF_IN_GA(.(f, X1), X2) → MAXF_IN_GA(X1, X2)
MAXF_IN_GA(.(t, X1), X2) → U5_GA(X1, X2, maxC_in_ga(X1, X2))
MAXF_IN_GA(.(t, X1), X2) → MAXC_IN_GA(X1, X2)
MAXSORTA_IN_GA(.(f, .(f, X1)), .(t, X2)) → U22_GA(X1, X2, maxcF_in_gg(X1, t))
U22_GA(X1, X2, maxcF_out_gg(X1, t)) → U23_GA(X1, X2, delJ_in_ga(X1, X3))
U22_GA(X1, X2, maxcF_out_gg(X1, t)) → DELJ_IN_GA(X1, X3)
DELJ_IN_GA(.(f, X1), .(f, X2)) → U6_GA(X1, X2, delJ_in_ga(X1, X2))
DELJ_IN_GA(.(f, X1), .(f, X2)) → DELJ_IN_GA(X1, X2)
MAXSORTA_IN_GA(.(f, .(f, X1)), .(X2, X3)) → U24_GA(X1, X2, X3, maxcF_in_ga(X1, X2))
U24_GA(X1, X2, X3, maxcF_out_ga(X1, X2)) → U25_GA(X1, X2, X3, delcG_in_gga(X2, X1, X4))
U25_GA(X1, X2, X3, delcG_out_gga(X2, X1, X4)) → U26_GA(X1, X2, X3, maxsortA_in_ga(X4, X3))
U25_GA(X1, X2, X3, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4, X3)
MAXSORTA_IN_GA(.(f, .(t, X1)), .(X2, X3)) → U27_GA(X1, X2, X3, maxC_in_ga(X1, X2))
MAXSORTA_IN_GA(.(f, .(t, X1)), .(X2, X3)) → MAXC_IN_GA(X1, X2)
MAXSORTA_IN_GA(.(f, .(t, X1)), .(t, X2)) → U28_GA(X1, X2, maxcC_in_gg(X1, t))
U28_GA(X1, X2, maxcC_out_gg(X1, t)) → U29_GA(X1, X2, delJ_in_ga(.(t, X1), X3))
U28_GA(X1, X2, maxcC_out_gg(X1, t)) → DELJ_IN_GA(.(t, X1), X3)
MAXSORTA_IN_GA(.(f, .(t, X1)), .(X2, X3)) → U30_GA(X1, X2, X3, maxcC_in_ga(X1, X2))
U30_GA(X1, X2, X3, maxcC_out_ga(X1, X2)) → U31_GA(X1, X2, X3, delcH_in_gga(X2, X1, X4))
U31_GA(X1, X2, X3, delcH_out_gga(X2, X1, X4)) → U32_GA(X1, X2, X3, maxsortA_in_ga(X4, X3))
U31_GA(X1, X2, X3, delcH_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4, X3)

The TRS R consists of the following rules:

delcB_in_ga(t, []) → delcB_out_ga(t, [])
delcB_in_ga(f, []) → delcB_out_ga(f, [])
maxcC_in_gg([], t) → maxcC_out_gg([], t)
maxcC_in_gg(.(t, X1), X2) → U48_gg(X1, X2, maxcC_in_gg(X1, X2))
maxcC_in_gg(.(f, X1), X2) → U49_gg(X1, X2, maxcC_in_gg(X1, X2))
U49_gg(X1, X2, maxcC_out_gg(X1, X2)) → maxcC_out_gg(.(f, X1), X2)
U48_gg(X1, X2, maxcC_out_gg(X1, X2)) → maxcC_out_gg(.(t, X1), X2)
maxcC_in_ga([], t) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1), X2) → U48_ga(X1, X2, maxcC_in_ga(X1, X2))
maxcC_in_ga(.(f, X1), X2) → U49_ga(X1, X2, maxcC_in_ga(X1, X2))
U49_ga(X1, X2, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, X2, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
delcD_in_gga(t, X1, .(t, X1)) → delcD_out_gga(t, X1, .(t, X1))
delcD_in_gga(f, X1, .(t, .(t, X2))) → U54_gga(X1, X2, delcI_in_ga(X1, X2))
delcI_in_ga([], []) → delcI_out_ga([], [])
delcI_in_ga(.(f, X1), X1) → delcI_out_ga(.(f, X1), X1)
delcI_in_ga(.(t, X1), .(t, X2)) → U50_ga(X1, X2, delcI_in_ga(X1, X2))
U50_ga(X1, X2, delcI_out_ga(X1, X2)) → delcI_out_ga(.(t, X1), .(t, X2))
U54_gga(X1, X2, delcI_out_ga(X1, X2)) → delcD_out_gga(f, X1, .(t, .(t, X2)))
delcE_in_gga(t, X1, .(f, X1)) → delcE_out_gga(t, X1, .(f, X1))
delcE_in_gga(f, X1, .(t, X2)) → U55_gga(X1, X2, delcI_in_ga(.(f, X1), X2))
U55_gga(X1, X2, delcI_out_ga(.(f, X1), X2)) → delcE_out_gga(f, X1, .(t, X2))
maxcF_in_gg([], f) → maxcF_out_gg([], f)
maxcF_in_gg(.(f, X1), X2) → U51_gg(X1, X2, maxcF_in_gg(X1, X2))
maxcF_in_gg(.(t, X1), X2) → U52_gg(X1, X2, maxcC_in_gg(X1, X2))
U52_gg(X1, X2, maxcC_out_gg(X1, X2)) → maxcF_out_gg(.(t, X1), X2)
U51_gg(X1, X2, maxcF_out_gg(X1, X2)) → maxcF_out_gg(.(f, X1), X2)
maxcF_in_ga([], f) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1), X2) → U51_ga(X1, X2, maxcF_in_ga(X1, X2))
maxcF_in_ga(.(t, X1), X2) → U52_ga(X1, X2, maxcC_in_ga(X1, X2))
U52_ga(X1, X2, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U51_ga(X1, X2, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
delcG_in_gga(f, X1, .(f, X1)) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1, .(f, .(f, X2))) → U56_gga(X1, X2, delcJ_in_ga(X1, X2))
delcJ_in_ga([], []) → delcJ_out_ga([], [])
delcJ_in_ga(.(t, X1), X1) → delcJ_out_ga(.(t, X1), X1)
delcJ_in_ga(.(f, X1), .(f, X2)) → U53_ga(X1, X2, delcJ_in_ga(X1, X2))
U53_ga(X1, X2, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))
U56_gga(X1, X2, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
delcH_in_gga(f, X1, .(t, X1)) → delcH_out_gga(f, X1, .(t, X1))
delcH_in_gga(t, X1, .(f, X2)) → U57_gga(X1, X2, delcJ_in_ga(.(t, X1), X2))
U57_gga(X1, X2, delcJ_out_ga(.(t, X1), X2)) → delcH_out_gga(t, X1, .(f, X2))

The argument filtering Pi contains the following mapping:
maxsortA_in_ga(x1, x2)  =  maxsortA_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
[]  =  []
delcB_in_ga(x1, x2)  =  delcB_in_ga(x1)
t  =  t
delcB_out_ga(x1, x2)  =  delcB_out_ga(x1, x2)
f  =  f
maxC_in_ga(x1, x2)  =  maxC_in_ga(x1)
maxcC_in_gg(x1, x2)  =  maxcC_in_gg(x1, x2)
maxcC_out_gg(x1, x2)  =  maxcC_out_gg(x1, x2)
U48_gg(x1, x2, x3)  =  U48_gg(x1, x2, x3)
U49_gg(x1, x2, x3)  =  U49_gg(x1, x2, x3)
delI_in_ga(x1, x2)  =  delI_in_ga(x1)
maxcC_in_ga(x1, x2)  =  maxcC_in_ga(x1)
maxcC_out_ga(x1, x2)  =  maxcC_out_ga(x1, x2)
U48_ga(x1, x2, x3)  =  U48_ga(x1, x3)
U49_ga(x1, x2, x3)  =  U49_ga(x1, x3)
delcD_in_gga(x1, x2, x3)  =  delcD_in_gga(x1, x2)
delcD_out_gga(x1, x2, x3)  =  delcD_out_gga(x1, x2, x3)
U54_gga(x1, x2, x3)  =  U54_gga(x1, x3)
delcI_in_ga(x1, x2)  =  delcI_in_ga(x1)
delcI_out_ga(x1, x2)  =  delcI_out_ga(x1, x2)
U50_ga(x1, x2, x3)  =  U50_ga(x1, x3)
delcE_in_gga(x1, x2, x3)  =  delcE_in_gga(x1, x2)
delcE_out_gga(x1, x2, x3)  =  delcE_out_gga(x1, x2, x3)
U55_gga(x1, x2, x3)  =  U55_gga(x1, x3)
maxF_in_ga(x1, x2)  =  maxF_in_ga(x1)
maxcF_in_gg(x1, x2)  =  maxcF_in_gg(x1, x2)
maxcF_out_gg(x1, x2)  =  maxcF_out_gg(x1, x2)
U51_gg(x1, x2, x3)  =  U51_gg(x1, x2, x3)
U52_gg(x1, x2, x3)  =  U52_gg(x1, x2, x3)
delJ_in_ga(x1, x2)  =  delJ_in_ga(x1)
maxcF_in_ga(x1, x2)  =  maxcF_in_ga(x1)
maxcF_out_ga(x1, x2)  =  maxcF_out_ga(x1, x2)
U51_ga(x1, x2, x3)  =  U51_ga(x1, x3)
U52_ga(x1, x2, x3)  =  U52_ga(x1, x3)
delcG_in_gga(x1, x2, x3)  =  delcG_in_gga(x1, x2)
delcG_out_gga(x1, x2, x3)  =  delcG_out_gga(x1, x2, x3)
U56_gga(x1, x2, x3)  =  U56_gga(x1, x3)
delcJ_in_ga(x1, x2)  =  delcJ_in_ga(x1)
delcJ_out_ga(x1, x2)  =  delcJ_out_ga(x1, x2)
U53_ga(x1, x2, x3)  =  U53_ga(x1, x3)
delcH_in_gga(x1, x2, x3)  =  delcH_in_gga(x1, x2)
delcH_out_gga(x1, x2, x3)  =  delcH_out_gga(x1, x2, x3)
U57_gga(x1, x2, x3)  =  U57_gga(x1, x3)
MAXSORTA_IN_GA(x1, x2)  =  MAXSORTA_IN_GA(x1)
U7_GA(x1, x2, x3)  =  U7_GA(x1, x3)
U8_GA(x1, x2, x3)  =  U8_GA(x1, x3)
U9_GA(x1, x2, x3, x4)  =  U9_GA(x1, x4)
MAXC_IN_GA(x1, x2)  =  MAXC_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x1, x3)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)
U10_GA(x1, x2, x3)  =  U10_GA(x1, x3)
U11_GA(x1, x2, x3)  =  U11_GA(x1, x3)
DELI_IN_GA(x1, x2)  =  DELI_IN_GA(x1)
U3_GA(x1, x2, x3)  =  U3_GA(x1, x3)
U12_GA(x1, x2, x3, x4)  =  U12_GA(x1, x4)
U13_GA(x1, x2, x3, x4)  =  U13_GA(x1, x4)
U14_GA(x1, x2, x3, x4)  =  U14_GA(x1, x4)
U15_GA(x1, x2, x3, x4)  =  U15_GA(x1, x4)
U16_GA(x1, x2, x3)  =  U16_GA(x1, x3)
U17_GA(x1, x2, x3)  =  U17_GA(x1, x3)
U18_GA(x1, x2, x3, x4)  =  U18_GA(x1, x4)
U19_GA(x1, x2, x3, x4)  =  U19_GA(x1, x4)
U20_GA(x1, x2, x3, x4)  =  U20_GA(x1, x4)
U21_GA(x1, x2, x3, x4)  =  U21_GA(x1, x4)
MAXF_IN_GA(x1, x2)  =  MAXF_IN_GA(x1)
U4_GA(x1, x2, x3)  =  U4_GA(x1, x3)
U5_GA(x1, x2, x3)  =  U5_GA(x1, x3)
U22_GA(x1, x2, x3)  =  U22_GA(x1, x3)
U23_GA(x1, x2, x3)  =  U23_GA(x1, x3)
DELJ_IN_GA(x1, x2)  =  DELJ_IN_GA(x1)
U6_GA(x1, x2, x3)  =  U6_GA(x1, x3)
U24_GA(x1, x2, x3, x4)  =  U24_GA(x1, x4)
U25_GA(x1, x2, x3, x4)  =  U25_GA(x1, x4)
U26_GA(x1, x2, x3, x4)  =  U26_GA(x1, x4)
U27_GA(x1, x2, x3, x4)  =  U27_GA(x1, x4)
U28_GA(x1, x2, x3)  =  U28_GA(x1, x3)
U29_GA(x1, x2, x3)  =  U29_GA(x1, x3)
U30_GA(x1, x2, x3, x4)  =  U30_GA(x1, x4)
U31_GA(x1, x2, x3, x4)  =  U31_GA(x1, x4)
U32_GA(x1, x2, x3, x4)  =  U32_GA(x1, x4)

We have to consider all (P,R,Pi)-chains

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MAXSORTA_IN_GA(.(X1, []), .(X1, X2)) → U7_GA(X1, X2, delcB_in_ga(X1, X3))
U7_GA(X1, X2, delcB_out_ga(X1, X3)) → U8_GA(X1, X2, maxsortA_in_ga(X3, X2))
U7_GA(X1, X2, delcB_out_ga(X1, X3)) → MAXSORTA_IN_GA(X3, X2)
MAXSORTA_IN_GA(.(t, .(t, X1)), .(X2, X3)) → U9_GA(X1, X2, X3, maxC_in_ga(X1, X2))
MAXSORTA_IN_GA(.(t, .(t, X1)), .(X2, X3)) → MAXC_IN_GA(X1, X2)
MAXC_IN_GA(.(t, X1), X2) → U1_GA(X1, X2, maxC_in_ga(X1, X2))
MAXC_IN_GA(.(t, X1), X2) → MAXC_IN_GA(X1, X2)
MAXC_IN_GA(.(f, X1), X2) → U2_GA(X1, X2, maxC_in_ga(X1, X2))
MAXC_IN_GA(.(f, X1), X2) → MAXC_IN_GA(X1, X2)
MAXSORTA_IN_GA(.(t, .(t, X1)), .(f, X2)) → U10_GA(X1, X2, maxcC_in_gg(X1, f))
U10_GA(X1, X2, maxcC_out_gg(X1, f)) → U11_GA(X1, X2, delI_in_ga(X1, X3))
U10_GA(X1, X2, maxcC_out_gg(X1, f)) → DELI_IN_GA(X1, X3)
DELI_IN_GA(.(t, X1), .(t, X2)) → U3_GA(X1, X2, delI_in_ga(X1, X2))
DELI_IN_GA(.(t, X1), .(t, X2)) → DELI_IN_GA(X1, X2)
MAXSORTA_IN_GA(.(t, .(t, X1)), .(X2, X3)) → U12_GA(X1, X2, X3, maxcC_in_ga(X1, X2))
U12_GA(X1, X2, X3, maxcC_out_ga(X1, X2)) → U13_GA(X1, X2, X3, delcD_in_gga(X2, X1, X4))
U13_GA(X1, X2, X3, delcD_out_gga(X2, X1, X4)) → U14_GA(X1, X2, X3, maxsortA_in_ga(X4, X3))
U13_GA(X1, X2, X3, delcD_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4, X3)
MAXSORTA_IN_GA(.(t, .(f, X1)), .(X2, X3)) → U15_GA(X1, X2, X3, maxC_in_ga(X1, X2))
MAXSORTA_IN_GA(.(t, .(f, X1)), .(X2, X3)) → MAXC_IN_GA(X1, X2)
MAXSORTA_IN_GA(.(t, .(f, X1)), .(f, X2)) → U16_GA(X1, X2, maxcC_in_gg(X1, f))
U16_GA(X1, X2, maxcC_out_gg(X1, f)) → U17_GA(X1, X2, delI_in_ga(.(f, X1), X3))
U16_GA(X1, X2, maxcC_out_gg(X1, f)) → DELI_IN_GA(.(f, X1), X3)
MAXSORTA_IN_GA(.(t, .(f, X1)), .(X2, X3)) → U18_GA(X1, X2, X3, maxcC_in_ga(X1, X2))
U18_GA(X1, X2, X3, maxcC_out_ga(X1, X2)) → U19_GA(X1, X2, X3, delcE_in_gga(X2, X1, X4))
U19_GA(X1, X2, X3, delcE_out_gga(X2, X1, X4)) → U20_GA(X1, X2, X3, maxsortA_in_ga(X4, X3))
U19_GA(X1, X2, X3, delcE_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4, X3)
MAXSORTA_IN_GA(.(f, .(f, X1)), .(X2, X3)) → U21_GA(X1, X2, X3, maxF_in_ga(X1, X2))
MAXSORTA_IN_GA(.(f, .(f, X1)), .(X2, X3)) → MAXF_IN_GA(X1, X2)
MAXF_IN_GA(.(f, X1), X2) → U4_GA(X1, X2, maxF_in_ga(X1, X2))
MAXF_IN_GA(.(f, X1), X2) → MAXF_IN_GA(X1, X2)
MAXF_IN_GA(.(t, X1), X2) → U5_GA(X1, X2, maxC_in_ga(X1, X2))
MAXF_IN_GA(.(t, X1), X2) → MAXC_IN_GA(X1, X2)
MAXSORTA_IN_GA(.(f, .(f, X1)), .(t, X2)) → U22_GA(X1, X2, maxcF_in_gg(X1, t))
U22_GA(X1, X2, maxcF_out_gg(X1, t)) → U23_GA(X1, X2, delJ_in_ga(X1, X3))
U22_GA(X1, X2, maxcF_out_gg(X1, t)) → DELJ_IN_GA(X1, X3)
DELJ_IN_GA(.(f, X1), .(f, X2)) → U6_GA(X1, X2, delJ_in_ga(X1, X2))
DELJ_IN_GA(.(f, X1), .(f, X2)) → DELJ_IN_GA(X1, X2)
MAXSORTA_IN_GA(.(f, .(f, X1)), .(X2, X3)) → U24_GA(X1, X2, X3, maxcF_in_ga(X1, X2))
U24_GA(X1, X2, X3, maxcF_out_ga(X1, X2)) → U25_GA(X1, X2, X3, delcG_in_gga(X2, X1, X4))
U25_GA(X1, X2, X3, delcG_out_gga(X2, X1, X4)) → U26_GA(X1, X2, X3, maxsortA_in_ga(X4, X3))
U25_GA(X1, X2, X3, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4, X3)
MAXSORTA_IN_GA(.(f, .(t, X1)), .(X2, X3)) → U27_GA(X1, X2, X3, maxC_in_ga(X1, X2))
MAXSORTA_IN_GA(.(f, .(t, X1)), .(X2, X3)) → MAXC_IN_GA(X1, X2)
MAXSORTA_IN_GA(.(f, .(t, X1)), .(t, X2)) → U28_GA(X1, X2, maxcC_in_gg(X1, t))
U28_GA(X1, X2, maxcC_out_gg(X1, t)) → U29_GA(X1, X2, delJ_in_ga(.(t, X1), X3))
U28_GA(X1, X2, maxcC_out_gg(X1, t)) → DELJ_IN_GA(.(t, X1), X3)
MAXSORTA_IN_GA(.(f, .(t, X1)), .(X2, X3)) → U30_GA(X1, X2, X3, maxcC_in_ga(X1, X2))
U30_GA(X1, X2, X3, maxcC_out_ga(X1, X2)) → U31_GA(X1, X2, X3, delcH_in_gga(X2, X1, X4))
U31_GA(X1, X2, X3, delcH_out_gga(X2, X1, X4)) → U32_GA(X1, X2, X3, maxsortA_in_ga(X4, X3))
U31_GA(X1, X2, X3, delcH_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4, X3)

The TRS R consists of the following rules:

delcB_in_ga(t, []) → delcB_out_ga(t, [])
delcB_in_ga(f, []) → delcB_out_ga(f, [])
maxcC_in_gg([], t) → maxcC_out_gg([], t)
maxcC_in_gg(.(t, X1), X2) → U48_gg(X1, X2, maxcC_in_gg(X1, X2))
maxcC_in_gg(.(f, X1), X2) → U49_gg(X1, X2, maxcC_in_gg(X1, X2))
U49_gg(X1, X2, maxcC_out_gg(X1, X2)) → maxcC_out_gg(.(f, X1), X2)
U48_gg(X1, X2, maxcC_out_gg(X1, X2)) → maxcC_out_gg(.(t, X1), X2)
maxcC_in_ga([], t) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1), X2) → U48_ga(X1, X2, maxcC_in_ga(X1, X2))
maxcC_in_ga(.(f, X1), X2) → U49_ga(X1, X2, maxcC_in_ga(X1, X2))
U49_ga(X1, X2, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, X2, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
delcD_in_gga(t, X1, .(t, X1)) → delcD_out_gga(t, X1, .(t, X1))
delcD_in_gga(f, X1, .(t, .(t, X2))) → U54_gga(X1, X2, delcI_in_ga(X1, X2))
delcI_in_ga([], []) → delcI_out_ga([], [])
delcI_in_ga(.(f, X1), X1) → delcI_out_ga(.(f, X1), X1)
delcI_in_ga(.(t, X1), .(t, X2)) → U50_ga(X1, X2, delcI_in_ga(X1, X2))
U50_ga(X1, X2, delcI_out_ga(X1, X2)) → delcI_out_ga(.(t, X1), .(t, X2))
U54_gga(X1, X2, delcI_out_ga(X1, X2)) → delcD_out_gga(f, X1, .(t, .(t, X2)))
delcE_in_gga(t, X1, .(f, X1)) → delcE_out_gga(t, X1, .(f, X1))
delcE_in_gga(f, X1, .(t, X2)) → U55_gga(X1, X2, delcI_in_ga(.(f, X1), X2))
U55_gga(X1, X2, delcI_out_ga(.(f, X1), X2)) → delcE_out_gga(f, X1, .(t, X2))
maxcF_in_gg([], f) → maxcF_out_gg([], f)
maxcF_in_gg(.(f, X1), X2) → U51_gg(X1, X2, maxcF_in_gg(X1, X2))
maxcF_in_gg(.(t, X1), X2) → U52_gg(X1, X2, maxcC_in_gg(X1, X2))
U52_gg(X1, X2, maxcC_out_gg(X1, X2)) → maxcF_out_gg(.(t, X1), X2)
U51_gg(X1, X2, maxcF_out_gg(X1, X2)) → maxcF_out_gg(.(f, X1), X2)
maxcF_in_ga([], f) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1), X2) → U51_ga(X1, X2, maxcF_in_ga(X1, X2))
maxcF_in_ga(.(t, X1), X2) → U52_ga(X1, X2, maxcC_in_ga(X1, X2))
U52_ga(X1, X2, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U51_ga(X1, X2, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
delcG_in_gga(f, X1, .(f, X1)) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1, .(f, .(f, X2))) → U56_gga(X1, X2, delcJ_in_ga(X1, X2))
delcJ_in_ga([], []) → delcJ_out_ga([], [])
delcJ_in_ga(.(t, X1), X1) → delcJ_out_ga(.(t, X1), X1)
delcJ_in_ga(.(f, X1), .(f, X2)) → U53_ga(X1, X2, delcJ_in_ga(X1, X2))
U53_ga(X1, X2, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))
U56_gga(X1, X2, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
delcH_in_gga(f, X1, .(t, X1)) → delcH_out_gga(f, X1, .(t, X1))
delcH_in_gga(t, X1, .(f, X2)) → U57_gga(X1, X2, delcJ_in_ga(.(t, X1), X2))
U57_gga(X1, X2, delcJ_out_ga(.(t, X1), X2)) → delcH_out_gga(t, X1, .(f, X2))

The argument filtering Pi contains the following mapping:
maxsortA_in_ga(x1, x2)  =  maxsortA_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
[]  =  []
delcB_in_ga(x1, x2)  =  delcB_in_ga(x1)
t  =  t
delcB_out_ga(x1, x2)  =  delcB_out_ga(x1, x2)
f  =  f
maxC_in_ga(x1, x2)  =  maxC_in_ga(x1)
maxcC_in_gg(x1, x2)  =  maxcC_in_gg(x1, x2)
maxcC_out_gg(x1, x2)  =  maxcC_out_gg(x1, x2)
U48_gg(x1, x2, x3)  =  U48_gg(x1, x2, x3)
U49_gg(x1, x2, x3)  =  U49_gg(x1, x2, x3)
delI_in_ga(x1, x2)  =  delI_in_ga(x1)
maxcC_in_ga(x1, x2)  =  maxcC_in_ga(x1)
maxcC_out_ga(x1, x2)  =  maxcC_out_ga(x1, x2)
U48_ga(x1, x2, x3)  =  U48_ga(x1, x3)
U49_ga(x1, x2, x3)  =  U49_ga(x1, x3)
delcD_in_gga(x1, x2, x3)  =  delcD_in_gga(x1, x2)
delcD_out_gga(x1, x2, x3)  =  delcD_out_gga(x1, x2, x3)
U54_gga(x1, x2, x3)  =  U54_gga(x1, x3)
delcI_in_ga(x1, x2)  =  delcI_in_ga(x1)
delcI_out_ga(x1, x2)  =  delcI_out_ga(x1, x2)
U50_ga(x1, x2, x3)  =  U50_ga(x1, x3)
delcE_in_gga(x1, x2, x3)  =  delcE_in_gga(x1, x2)
delcE_out_gga(x1, x2, x3)  =  delcE_out_gga(x1, x2, x3)
U55_gga(x1, x2, x3)  =  U55_gga(x1, x3)
maxF_in_ga(x1, x2)  =  maxF_in_ga(x1)
maxcF_in_gg(x1, x2)  =  maxcF_in_gg(x1, x2)
maxcF_out_gg(x1, x2)  =  maxcF_out_gg(x1, x2)
U51_gg(x1, x2, x3)  =  U51_gg(x1, x2, x3)
U52_gg(x1, x2, x3)  =  U52_gg(x1, x2, x3)
delJ_in_ga(x1, x2)  =  delJ_in_ga(x1)
maxcF_in_ga(x1, x2)  =  maxcF_in_ga(x1)
maxcF_out_ga(x1, x2)  =  maxcF_out_ga(x1, x2)
U51_ga(x1, x2, x3)  =  U51_ga(x1, x3)
U52_ga(x1, x2, x3)  =  U52_ga(x1, x3)
delcG_in_gga(x1, x2, x3)  =  delcG_in_gga(x1, x2)
delcG_out_gga(x1, x2, x3)  =  delcG_out_gga(x1, x2, x3)
U56_gga(x1, x2, x3)  =  U56_gga(x1, x3)
delcJ_in_ga(x1, x2)  =  delcJ_in_ga(x1)
delcJ_out_ga(x1, x2)  =  delcJ_out_ga(x1, x2)
U53_ga(x1, x2, x3)  =  U53_ga(x1, x3)
delcH_in_gga(x1, x2, x3)  =  delcH_in_gga(x1, x2)
delcH_out_gga(x1, x2, x3)  =  delcH_out_gga(x1, x2, x3)
U57_gga(x1, x2, x3)  =  U57_gga(x1, x3)
MAXSORTA_IN_GA(x1, x2)  =  MAXSORTA_IN_GA(x1)
U7_GA(x1, x2, x3)  =  U7_GA(x1, x3)
U8_GA(x1, x2, x3)  =  U8_GA(x1, x3)
U9_GA(x1, x2, x3, x4)  =  U9_GA(x1, x4)
MAXC_IN_GA(x1, x2)  =  MAXC_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x1, x3)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)
U10_GA(x1, x2, x3)  =  U10_GA(x1, x3)
U11_GA(x1, x2, x3)  =  U11_GA(x1, x3)
DELI_IN_GA(x1, x2)  =  DELI_IN_GA(x1)
U3_GA(x1, x2, x3)  =  U3_GA(x1, x3)
U12_GA(x1, x2, x3, x4)  =  U12_GA(x1, x4)
U13_GA(x1, x2, x3, x4)  =  U13_GA(x1, x4)
U14_GA(x1, x2, x3, x4)  =  U14_GA(x1, x4)
U15_GA(x1, x2, x3, x4)  =  U15_GA(x1, x4)
U16_GA(x1, x2, x3)  =  U16_GA(x1, x3)
U17_GA(x1, x2, x3)  =  U17_GA(x1, x3)
U18_GA(x1, x2, x3, x4)  =  U18_GA(x1, x4)
U19_GA(x1, x2, x3, x4)  =  U19_GA(x1, x4)
U20_GA(x1, x2, x3, x4)  =  U20_GA(x1, x4)
U21_GA(x1, x2, x3, x4)  =  U21_GA(x1, x4)
MAXF_IN_GA(x1, x2)  =  MAXF_IN_GA(x1)
U4_GA(x1, x2, x3)  =  U4_GA(x1, x3)
U5_GA(x1, x2, x3)  =  U5_GA(x1, x3)
U22_GA(x1, x2, x3)  =  U22_GA(x1, x3)
U23_GA(x1, x2, x3)  =  U23_GA(x1, x3)
DELJ_IN_GA(x1, x2)  =  DELJ_IN_GA(x1)
U6_GA(x1, x2, x3)  =  U6_GA(x1, x3)
U24_GA(x1, x2, x3, x4)  =  U24_GA(x1, x4)
U25_GA(x1, x2, x3, x4)  =  U25_GA(x1, x4)
U26_GA(x1, x2, x3, x4)  =  U26_GA(x1, x4)
U27_GA(x1, x2, x3, x4)  =  U27_GA(x1, x4)
U28_GA(x1, x2, x3)  =  U28_GA(x1, x3)
U29_GA(x1, x2, x3)  =  U29_GA(x1, x3)
U30_GA(x1, x2, x3, x4)  =  U30_GA(x1, x4)
U31_GA(x1, x2, x3, x4)  =  U31_GA(x1, x4)
U32_GA(x1, x2, x3, x4)  =  U32_GA(x1, x4)

We have to consider all (P,R,Pi)-chains

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 5 SCCs with 32 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

DELJ_IN_GA(.(f, X1), .(f, X2)) → DELJ_IN_GA(X1, X2)

The TRS R consists of the following rules:

delcB_in_ga(t, []) → delcB_out_ga(t, [])
delcB_in_ga(f, []) → delcB_out_ga(f, [])
maxcC_in_gg([], t) → maxcC_out_gg([], t)
maxcC_in_gg(.(t, X1), X2) → U48_gg(X1, X2, maxcC_in_gg(X1, X2))
maxcC_in_gg(.(f, X1), X2) → U49_gg(X1, X2, maxcC_in_gg(X1, X2))
U49_gg(X1, X2, maxcC_out_gg(X1, X2)) → maxcC_out_gg(.(f, X1), X2)
U48_gg(X1, X2, maxcC_out_gg(X1, X2)) → maxcC_out_gg(.(t, X1), X2)
maxcC_in_ga([], t) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1), X2) → U48_ga(X1, X2, maxcC_in_ga(X1, X2))
maxcC_in_ga(.(f, X1), X2) → U49_ga(X1, X2, maxcC_in_ga(X1, X2))
U49_ga(X1, X2, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, X2, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
delcD_in_gga(t, X1, .(t, X1)) → delcD_out_gga(t, X1, .(t, X1))
delcD_in_gga(f, X1, .(t, .(t, X2))) → U54_gga(X1, X2, delcI_in_ga(X1, X2))
delcI_in_ga([], []) → delcI_out_ga([], [])
delcI_in_ga(.(f, X1), X1) → delcI_out_ga(.(f, X1), X1)
delcI_in_ga(.(t, X1), .(t, X2)) → U50_ga(X1, X2, delcI_in_ga(X1, X2))
U50_ga(X1, X2, delcI_out_ga(X1, X2)) → delcI_out_ga(.(t, X1), .(t, X2))
U54_gga(X1, X2, delcI_out_ga(X1, X2)) → delcD_out_gga(f, X1, .(t, .(t, X2)))
delcE_in_gga(t, X1, .(f, X1)) → delcE_out_gga(t, X1, .(f, X1))
delcE_in_gga(f, X1, .(t, X2)) → U55_gga(X1, X2, delcI_in_ga(.(f, X1), X2))
U55_gga(X1, X2, delcI_out_ga(.(f, X1), X2)) → delcE_out_gga(f, X1, .(t, X2))
maxcF_in_gg([], f) → maxcF_out_gg([], f)
maxcF_in_gg(.(f, X1), X2) → U51_gg(X1, X2, maxcF_in_gg(X1, X2))
maxcF_in_gg(.(t, X1), X2) → U52_gg(X1, X2, maxcC_in_gg(X1, X2))
U52_gg(X1, X2, maxcC_out_gg(X1, X2)) → maxcF_out_gg(.(t, X1), X2)
U51_gg(X1, X2, maxcF_out_gg(X1, X2)) → maxcF_out_gg(.(f, X1), X2)
maxcF_in_ga([], f) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1), X2) → U51_ga(X1, X2, maxcF_in_ga(X1, X2))
maxcF_in_ga(.(t, X1), X2) → U52_ga(X1, X2, maxcC_in_ga(X1, X2))
U52_ga(X1, X2, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U51_ga(X1, X2, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
delcG_in_gga(f, X1, .(f, X1)) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1, .(f, .(f, X2))) → U56_gga(X1, X2, delcJ_in_ga(X1, X2))
delcJ_in_ga([], []) → delcJ_out_ga([], [])
delcJ_in_ga(.(t, X1), X1) → delcJ_out_ga(.(t, X1), X1)
delcJ_in_ga(.(f, X1), .(f, X2)) → U53_ga(X1, X2, delcJ_in_ga(X1, X2))
U53_ga(X1, X2, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))
U56_gga(X1, X2, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
delcH_in_gga(f, X1, .(t, X1)) → delcH_out_gga(f, X1, .(t, X1))
delcH_in_gga(t, X1, .(f, X2)) → U57_gga(X1, X2, delcJ_in_ga(.(t, X1), X2))
U57_gga(X1, X2, delcJ_out_ga(.(t, X1), X2)) → delcH_out_gga(t, X1, .(f, X2))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
[]  =  []
delcB_in_ga(x1, x2)  =  delcB_in_ga(x1)
t  =  t
delcB_out_ga(x1, x2)  =  delcB_out_ga(x1, x2)
f  =  f
maxcC_in_gg(x1, x2)  =  maxcC_in_gg(x1, x2)
maxcC_out_gg(x1, x2)  =  maxcC_out_gg(x1, x2)
U48_gg(x1, x2, x3)  =  U48_gg(x1, x2, x3)
U49_gg(x1, x2, x3)  =  U49_gg(x1, x2, x3)
maxcC_in_ga(x1, x2)  =  maxcC_in_ga(x1)
maxcC_out_ga(x1, x2)  =  maxcC_out_ga(x1, x2)
U48_ga(x1, x2, x3)  =  U48_ga(x1, x3)
U49_ga(x1, x2, x3)  =  U49_ga(x1, x3)
delcD_in_gga(x1, x2, x3)  =  delcD_in_gga(x1, x2)
delcD_out_gga(x1, x2, x3)  =  delcD_out_gga(x1, x2, x3)
U54_gga(x1, x2, x3)  =  U54_gga(x1, x3)
delcI_in_ga(x1, x2)  =  delcI_in_ga(x1)
delcI_out_ga(x1, x2)  =  delcI_out_ga(x1, x2)
U50_ga(x1, x2, x3)  =  U50_ga(x1, x3)
delcE_in_gga(x1, x2, x3)  =  delcE_in_gga(x1, x2)
delcE_out_gga(x1, x2, x3)  =  delcE_out_gga(x1, x2, x3)
U55_gga(x1, x2, x3)  =  U55_gga(x1, x3)
maxcF_in_gg(x1, x2)  =  maxcF_in_gg(x1, x2)
maxcF_out_gg(x1, x2)  =  maxcF_out_gg(x1, x2)
U51_gg(x1, x2, x3)  =  U51_gg(x1, x2, x3)
U52_gg(x1, x2, x3)  =  U52_gg(x1, x2, x3)
maxcF_in_ga(x1, x2)  =  maxcF_in_ga(x1)
maxcF_out_ga(x1, x2)  =  maxcF_out_ga(x1, x2)
U51_ga(x1, x2, x3)  =  U51_ga(x1, x3)
U52_ga(x1, x2, x3)  =  U52_ga(x1, x3)
delcG_in_gga(x1, x2, x3)  =  delcG_in_gga(x1, x2)
delcG_out_gga(x1, x2, x3)  =  delcG_out_gga(x1, x2, x3)
U56_gga(x1, x2, x3)  =  U56_gga(x1, x3)
delcJ_in_ga(x1, x2)  =  delcJ_in_ga(x1)
delcJ_out_ga(x1, x2)  =  delcJ_out_ga(x1, x2)
U53_ga(x1, x2, x3)  =  U53_ga(x1, x3)
delcH_in_gga(x1, x2, x3)  =  delcH_in_gga(x1, x2)
delcH_out_gga(x1, x2, x3)  =  delcH_out_gga(x1, x2, x3)
U57_gga(x1, x2, x3)  =  U57_gga(x1, x3)
DELJ_IN_GA(x1, x2)  =  DELJ_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(8) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

DELJ_IN_GA(.(f, X1), .(f, X2)) → DELJ_IN_GA(X1, X2)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
f  =  f
DELJ_IN_GA(x1, x2)  =  DELJ_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(10) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(11) Obligation:

Q DP problem:
The TRS P consists of the following rules:

DELJ_IN_GA(.(f, X1)) → DELJ_IN_GA(X1)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(12) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • DELJ_IN_GA(.(f, X1)) → DELJ_IN_GA(X1)
    The graph contains the following edges 1 > 1

(13) YES

(14) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

DELI_IN_GA(.(t, X1), .(t, X2)) → DELI_IN_GA(X1, X2)

The TRS R consists of the following rules:

delcB_in_ga(t, []) → delcB_out_ga(t, [])
delcB_in_ga(f, []) → delcB_out_ga(f, [])
maxcC_in_gg([], t) → maxcC_out_gg([], t)
maxcC_in_gg(.(t, X1), X2) → U48_gg(X1, X2, maxcC_in_gg(X1, X2))
maxcC_in_gg(.(f, X1), X2) → U49_gg(X1, X2, maxcC_in_gg(X1, X2))
U49_gg(X1, X2, maxcC_out_gg(X1, X2)) → maxcC_out_gg(.(f, X1), X2)
U48_gg(X1, X2, maxcC_out_gg(X1, X2)) → maxcC_out_gg(.(t, X1), X2)
maxcC_in_ga([], t) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1), X2) → U48_ga(X1, X2, maxcC_in_ga(X1, X2))
maxcC_in_ga(.(f, X1), X2) → U49_ga(X1, X2, maxcC_in_ga(X1, X2))
U49_ga(X1, X2, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, X2, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
delcD_in_gga(t, X1, .(t, X1)) → delcD_out_gga(t, X1, .(t, X1))
delcD_in_gga(f, X1, .(t, .(t, X2))) → U54_gga(X1, X2, delcI_in_ga(X1, X2))
delcI_in_ga([], []) → delcI_out_ga([], [])
delcI_in_ga(.(f, X1), X1) → delcI_out_ga(.(f, X1), X1)
delcI_in_ga(.(t, X1), .(t, X2)) → U50_ga(X1, X2, delcI_in_ga(X1, X2))
U50_ga(X1, X2, delcI_out_ga(X1, X2)) → delcI_out_ga(.(t, X1), .(t, X2))
U54_gga(X1, X2, delcI_out_ga(X1, X2)) → delcD_out_gga(f, X1, .(t, .(t, X2)))
delcE_in_gga(t, X1, .(f, X1)) → delcE_out_gga(t, X1, .(f, X1))
delcE_in_gga(f, X1, .(t, X2)) → U55_gga(X1, X2, delcI_in_ga(.(f, X1), X2))
U55_gga(X1, X2, delcI_out_ga(.(f, X1), X2)) → delcE_out_gga(f, X1, .(t, X2))
maxcF_in_gg([], f) → maxcF_out_gg([], f)
maxcF_in_gg(.(f, X1), X2) → U51_gg(X1, X2, maxcF_in_gg(X1, X2))
maxcF_in_gg(.(t, X1), X2) → U52_gg(X1, X2, maxcC_in_gg(X1, X2))
U52_gg(X1, X2, maxcC_out_gg(X1, X2)) → maxcF_out_gg(.(t, X1), X2)
U51_gg(X1, X2, maxcF_out_gg(X1, X2)) → maxcF_out_gg(.(f, X1), X2)
maxcF_in_ga([], f) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1), X2) → U51_ga(X1, X2, maxcF_in_ga(X1, X2))
maxcF_in_ga(.(t, X1), X2) → U52_ga(X1, X2, maxcC_in_ga(X1, X2))
U52_ga(X1, X2, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U51_ga(X1, X2, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
delcG_in_gga(f, X1, .(f, X1)) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1, .(f, .(f, X2))) → U56_gga(X1, X2, delcJ_in_ga(X1, X2))
delcJ_in_ga([], []) → delcJ_out_ga([], [])
delcJ_in_ga(.(t, X1), X1) → delcJ_out_ga(.(t, X1), X1)
delcJ_in_ga(.(f, X1), .(f, X2)) → U53_ga(X1, X2, delcJ_in_ga(X1, X2))
U53_ga(X1, X2, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))
U56_gga(X1, X2, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
delcH_in_gga(f, X1, .(t, X1)) → delcH_out_gga(f, X1, .(t, X1))
delcH_in_gga(t, X1, .(f, X2)) → U57_gga(X1, X2, delcJ_in_ga(.(t, X1), X2))
U57_gga(X1, X2, delcJ_out_ga(.(t, X1), X2)) → delcH_out_gga(t, X1, .(f, X2))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
[]  =  []
delcB_in_ga(x1, x2)  =  delcB_in_ga(x1)
t  =  t
delcB_out_ga(x1, x2)  =  delcB_out_ga(x1, x2)
f  =  f
maxcC_in_gg(x1, x2)  =  maxcC_in_gg(x1, x2)
maxcC_out_gg(x1, x2)  =  maxcC_out_gg(x1, x2)
U48_gg(x1, x2, x3)  =  U48_gg(x1, x2, x3)
U49_gg(x1, x2, x3)  =  U49_gg(x1, x2, x3)
maxcC_in_ga(x1, x2)  =  maxcC_in_ga(x1)
maxcC_out_ga(x1, x2)  =  maxcC_out_ga(x1, x2)
U48_ga(x1, x2, x3)  =  U48_ga(x1, x3)
U49_ga(x1, x2, x3)  =  U49_ga(x1, x3)
delcD_in_gga(x1, x2, x3)  =  delcD_in_gga(x1, x2)
delcD_out_gga(x1, x2, x3)  =  delcD_out_gga(x1, x2, x3)
U54_gga(x1, x2, x3)  =  U54_gga(x1, x3)
delcI_in_ga(x1, x2)  =  delcI_in_ga(x1)
delcI_out_ga(x1, x2)  =  delcI_out_ga(x1, x2)
U50_ga(x1, x2, x3)  =  U50_ga(x1, x3)
delcE_in_gga(x1, x2, x3)  =  delcE_in_gga(x1, x2)
delcE_out_gga(x1, x2, x3)  =  delcE_out_gga(x1, x2, x3)
U55_gga(x1, x2, x3)  =  U55_gga(x1, x3)
maxcF_in_gg(x1, x2)  =  maxcF_in_gg(x1, x2)
maxcF_out_gg(x1, x2)  =  maxcF_out_gg(x1, x2)
U51_gg(x1, x2, x3)  =  U51_gg(x1, x2, x3)
U52_gg(x1, x2, x3)  =  U52_gg(x1, x2, x3)
maxcF_in_ga(x1, x2)  =  maxcF_in_ga(x1)
maxcF_out_ga(x1, x2)  =  maxcF_out_ga(x1, x2)
U51_ga(x1, x2, x3)  =  U51_ga(x1, x3)
U52_ga(x1, x2, x3)  =  U52_ga(x1, x3)
delcG_in_gga(x1, x2, x3)  =  delcG_in_gga(x1, x2)
delcG_out_gga(x1, x2, x3)  =  delcG_out_gga(x1, x2, x3)
U56_gga(x1, x2, x3)  =  U56_gga(x1, x3)
delcJ_in_ga(x1, x2)  =  delcJ_in_ga(x1)
delcJ_out_ga(x1, x2)  =  delcJ_out_ga(x1, x2)
U53_ga(x1, x2, x3)  =  U53_ga(x1, x3)
delcH_in_gga(x1, x2, x3)  =  delcH_in_gga(x1, x2)
delcH_out_gga(x1, x2, x3)  =  delcH_out_gga(x1, x2, x3)
U57_gga(x1, x2, x3)  =  U57_gga(x1, x3)
DELI_IN_GA(x1, x2)  =  DELI_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(15) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(16) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

DELI_IN_GA(.(t, X1), .(t, X2)) → DELI_IN_GA(X1, X2)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
t  =  t
DELI_IN_GA(x1, x2)  =  DELI_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(17) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(18) Obligation:

Q DP problem:
The TRS P consists of the following rules:

DELI_IN_GA(.(t, X1)) → DELI_IN_GA(X1)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(19) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • DELI_IN_GA(.(t, X1)) → DELI_IN_GA(X1)
    The graph contains the following edges 1 > 1

(20) YES

(21) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MAXC_IN_GA(.(f, X1), X2) → MAXC_IN_GA(X1, X2)
MAXC_IN_GA(.(t, X1), X2) → MAXC_IN_GA(X1, X2)

The TRS R consists of the following rules:

delcB_in_ga(t, []) → delcB_out_ga(t, [])
delcB_in_ga(f, []) → delcB_out_ga(f, [])
maxcC_in_gg([], t) → maxcC_out_gg([], t)
maxcC_in_gg(.(t, X1), X2) → U48_gg(X1, X2, maxcC_in_gg(X1, X2))
maxcC_in_gg(.(f, X1), X2) → U49_gg(X1, X2, maxcC_in_gg(X1, X2))
U49_gg(X1, X2, maxcC_out_gg(X1, X2)) → maxcC_out_gg(.(f, X1), X2)
U48_gg(X1, X2, maxcC_out_gg(X1, X2)) → maxcC_out_gg(.(t, X1), X2)
maxcC_in_ga([], t) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1), X2) → U48_ga(X1, X2, maxcC_in_ga(X1, X2))
maxcC_in_ga(.(f, X1), X2) → U49_ga(X1, X2, maxcC_in_ga(X1, X2))
U49_ga(X1, X2, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, X2, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
delcD_in_gga(t, X1, .(t, X1)) → delcD_out_gga(t, X1, .(t, X1))
delcD_in_gga(f, X1, .(t, .(t, X2))) → U54_gga(X1, X2, delcI_in_ga(X1, X2))
delcI_in_ga([], []) → delcI_out_ga([], [])
delcI_in_ga(.(f, X1), X1) → delcI_out_ga(.(f, X1), X1)
delcI_in_ga(.(t, X1), .(t, X2)) → U50_ga(X1, X2, delcI_in_ga(X1, X2))
U50_ga(X1, X2, delcI_out_ga(X1, X2)) → delcI_out_ga(.(t, X1), .(t, X2))
U54_gga(X1, X2, delcI_out_ga(X1, X2)) → delcD_out_gga(f, X1, .(t, .(t, X2)))
delcE_in_gga(t, X1, .(f, X1)) → delcE_out_gga(t, X1, .(f, X1))
delcE_in_gga(f, X1, .(t, X2)) → U55_gga(X1, X2, delcI_in_ga(.(f, X1), X2))
U55_gga(X1, X2, delcI_out_ga(.(f, X1), X2)) → delcE_out_gga(f, X1, .(t, X2))
maxcF_in_gg([], f) → maxcF_out_gg([], f)
maxcF_in_gg(.(f, X1), X2) → U51_gg(X1, X2, maxcF_in_gg(X1, X2))
maxcF_in_gg(.(t, X1), X2) → U52_gg(X1, X2, maxcC_in_gg(X1, X2))
U52_gg(X1, X2, maxcC_out_gg(X1, X2)) → maxcF_out_gg(.(t, X1), X2)
U51_gg(X1, X2, maxcF_out_gg(X1, X2)) → maxcF_out_gg(.(f, X1), X2)
maxcF_in_ga([], f) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1), X2) → U51_ga(X1, X2, maxcF_in_ga(X1, X2))
maxcF_in_ga(.(t, X1), X2) → U52_ga(X1, X2, maxcC_in_ga(X1, X2))
U52_ga(X1, X2, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U51_ga(X1, X2, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
delcG_in_gga(f, X1, .(f, X1)) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1, .(f, .(f, X2))) → U56_gga(X1, X2, delcJ_in_ga(X1, X2))
delcJ_in_ga([], []) → delcJ_out_ga([], [])
delcJ_in_ga(.(t, X1), X1) → delcJ_out_ga(.(t, X1), X1)
delcJ_in_ga(.(f, X1), .(f, X2)) → U53_ga(X1, X2, delcJ_in_ga(X1, X2))
U53_ga(X1, X2, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))
U56_gga(X1, X2, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
delcH_in_gga(f, X1, .(t, X1)) → delcH_out_gga(f, X1, .(t, X1))
delcH_in_gga(t, X1, .(f, X2)) → U57_gga(X1, X2, delcJ_in_ga(.(t, X1), X2))
U57_gga(X1, X2, delcJ_out_ga(.(t, X1), X2)) → delcH_out_gga(t, X1, .(f, X2))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
[]  =  []
delcB_in_ga(x1, x2)  =  delcB_in_ga(x1)
t  =  t
delcB_out_ga(x1, x2)  =  delcB_out_ga(x1, x2)
f  =  f
maxcC_in_gg(x1, x2)  =  maxcC_in_gg(x1, x2)
maxcC_out_gg(x1, x2)  =  maxcC_out_gg(x1, x2)
U48_gg(x1, x2, x3)  =  U48_gg(x1, x2, x3)
U49_gg(x1, x2, x3)  =  U49_gg(x1, x2, x3)
maxcC_in_ga(x1, x2)  =  maxcC_in_ga(x1)
maxcC_out_ga(x1, x2)  =  maxcC_out_ga(x1, x2)
U48_ga(x1, x2, x3)  =  U48_ga(x1, x3)
U49_ga(x1, x2, x3)  =  U49_ga(x1, x3)
delcD_in_gga(x1, x2, x3)  =  delcD_in_gga(x1, x2)
delcD_out_gga(x1, x2, x3)  =  delcD_out_gga(x1, x2, x3)
U54_gga(x1, x2, x3)  =  U54_gga(x1, x3)
delcI_in_ga(x1, x2)  =  delcI_in_ga(x1)
delcI_out_ga(x1, x2)  =  delcI_out_ga(x1, x2)
U50_ga(x1, x2, x3)  =  U50_ga(x1, x3)
delcE_in_gga(x1, x2, x3)  =  delcE_in_gga(x1, x2)
delcE_out_gga(x1, x2, x3)  =  delcE_out_gga(x1, x2, x3)
U55_gga(x1, x2, x3)  =  U55_gga(x1, x3)
maxcF_in_gg(x1, x2)  =  maxcF_in_gg(x1, x2)
maxcF_out_gg(x1, x2)  =  maxcF_out_gg(x1, x2)
U51_gg(x1, x2, x3)  =  U51_gg(x1, x2, x3)
U52_gg(x1, x2, x3)  =  U52_gg(x1, x2, x3)
maxcF_in_ga(x1, x2)  =  maxcF_in_ga(x1)
maxcF_out_ga(x1, x2)  =  maxcF_out_ga(x1, x2)
U51_ga(x1, x2, x3)  =  U51_ga(x1, x3)
U52_ga(x1, x2, x3)  =  U52_ga(x1, x3)
delcG_in_gga(x1, x2, x3)  =  delcG_in_gga(x1, x2)
delcG_out_gga(x1, x2, x3)  =  delcG_out_gga(x1, x2, x3)
U56_gga(x1, x2, x3)  =  U56_gga(x1, x3)
delcJ_in_ga(x1, x2)  =  delcJ_in_ga(x1)
delcJ_out_ga(x1, x2)  =  delcJ_out_ga(x1, x2)
U53_ga(x1, x2, x3)  =  U53_ga(x1, x3)
delcH_in_gga(x1, x2, x3)  =  delcH_in_gga(x1, x2)
delcH_out_gga(x1, x2, x3)  =  delcH_out_gga(x1, x2, x3)
U57_gga(x1, x2, x3)  =  U57_gga(x1, x3)
MAXC_IN_GA(x1, x2)  =  MAXC_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(22) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(23) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MAXC_IN_GA(.(f, X1), X2) → MAXC_IN_GA(X1, X2)
MAXC_IN_GA(.(t, X1), X2) → MAXC_IN_GA(X1, X2)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
t  =  t
f  =  f
MAXC_IN_GA(x1, x2)  =  MAXC_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(24) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(25) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MAXC_IN_GA(.(f, X1)) → MAXC_IN_GA(X1)
MAXC_IN_GA(.(t, X1)) → MAXC_IN_GA(X1)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(26) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • MAXC_IN_GA(.(f, X1)) → MAXC_IN_GA(X1)
    The graph contains the following edges 1 > 1

  • MAXC_IN_GA(.(t, X1)) → MAXC_IN_GA(X1)
    The graph contains the following edges 1 > 1

(27) YES

(28) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MAXF_IN_GA(.(f, X1), X2) → MAXF_IN_GA(X1, X2)

The TRS R consists of the following rules:

delcB_in_ga(t, []) → delcB_out_ga(t, [])
delcB_in_ga(f, []) → delcB_out_ga(f, [])
maxcC_in_gg([], t) → maxcC_out_gg([], t)
maxcC_in_gg(.(t, X1), X2) → U48_gg(X1, X2, maxcC_in_gg(X1, X2))
maxcC_in_gg(.(f, X1), X2) → U49_gg(X1, X2, maxcC_in_gg(X1, X2))
U49_gg(X1, X2, maxcC_out_gg(X1, X2)) → maxcC_out_gg(.(f, X1), X2)
U48_gg(X1, X2, maxcC_out_gg(X1, X2)) → maxcC_out_gg(.(t, X1), X2)
maxcC_in_ga([], t) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1), X2) → U48_ga(X1, X2, maxcC_in_ga(X1, X2))
maxcC_in_ga(.(f, X1), X2) → U49_ga(X1, X2, maxcC_in_ga(X1, X2))
U49_ga(X1, X2, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, X2, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
delcD_in_gga(t, X1, .(t, X1)) → delcD_out_gga(t, X1, .(t, X1))
delcD_in_gga(f, X1, .(t, .(t, X2))) → U54_gga(X1, X2, delcI_in_ga(X1, X2))
delcI_in_ga([], []) → delcI_out_ga([], [])
delcI_in_ga(.(f, X1), X1) → delcI_out_ga(.(f, X1), X1)
delcI_in_ga(.(t, X1), .(t, X2)) → U50_ga(X1, X2, delcI_in_ga(X1, X2))
U50_ga(X1, X2, delcI_out_ga(X1, X2)) → delcI_out_ga(.(t, X1), .(t, X2))
U54_gga(X1, X2, delcI_out_ga(X1, X2)) → delcD_out_gga(f, X1, .(t, .(t, X2)))
delcE_in_gga(t, X1, .(f, X1)) → delcE_out_gga(t, X1, .(f, X1))
delcE_in_gga(f, X1, .(t, X2)) → U55_gga(X1, X2, delcI_in_ga(.(f, X1), X2))
U55_gga(X1, X2, delcI_out_ga(.(f, X1), X2)) → delcE_out_gga(f, X1, .(t, X2))
maxcF_in_gg([], f) → maxcF_out_gg([], f)
maxcF_in_gg(.(f, X1), X2) → U51_gg(X1, X2, maxcF_in_gg(X1, X2))
maxcF_in_gg(.(t, X1), X2) → U52_gg(X1, X2, maxcC_in_gg(X1, X2))
U52_gg(X1, X2, maxcC_out_gg(X1, X2)) → maxcF_out_gg(.(t, X1), X2)
U51_gg(X1, X2, maxcF_out_gg(X1, X2)) → maxcF_out_gg(.(f, X1), X2)
maxcF_in_ga([], f) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1), X2) → U51_ga(X1, X2, maxcF_in_ga(X1, X2))
maxcF_in_ga(.(t, X1), X2) → U52_ga(X1, X2, maxcC_in_ga(X1, X2))
U52_ga(X1, X2, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U51_ga(X1, X2, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
delcG_in_gga(f, X1, .(f, X1)) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1, .(f, .(f, X2))) → U56_gga(X1, X2, delcJ_in_ga(X1, X2))
delcJ_in_ga([], []) → delcJ_out_ga([], [])
delcJ_in_ga(.(t, X1), X1) → delcJ_out_ga(.(t, X1), X1)
delcJ_in_ga(.(f, X1), .(f, X2)) → U53_ga(X1, X2, delcJ_in_ga(X1, X2))
U53_ga(X1, X2, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))
U56_gga(X1, X2, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
delcH_in_gga(f, X1, .(t, X1)) → delcH_out_gga(f, X1, .(t, X1))
delcH_in_gga(t, X1, .(f, X2)) → U57_gga(X1, X2, delcJ_in_ga(.(t, X1), X2))
U57_gga(X1, X2, delcJ_out_ga(.(t, X1), X2)) → delcH_out_gga(t, X1, .(f, X2))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
[]  =  []
delcB_in_ga(x1, x2)  =  delcB_in_ga(x1)
t  =  t
delcB_out_ga(x1, x2)  =  delcB_out_ga(x1, x2)
f  =  f
maxcC_in_gg(x1, x2)  =  maxcC_in_gg(x1, x2)
maxcC_out_gg(x1, x2)  =  maxcC_out_gg(x1, x2)
U48_gg(x1, x2, x3)  =  U48_gg(x1, x2, x3)
U49_gg(x1, x2, x3)  =  U49_gg(x1, x2, x3)
maxcC_in_ga(x1, x2)  =  maxcC_in_ga(x1)
maxcC_out_ga(x1, x2)  =  maxcC_out_ga(x1, x2)
U48_ga(x1, x2, x3)  =  U48_ga(x1, x3)
U49_ga(x1, x2, x3)  =  U49_ga(x1, x3)
delcD_in_gga(x1, x2, x3)  =  delcD_in_gga(x1, x2)
delcD_out_gga(x1, x2, x3)  =  delcD_out_gga(x1, x2, x3)
U54_gga(x1, x2, x3)  =  U54_gga(x1, x3)
delcI_in_ga(x1, x2)  =  delcI_in_ga(x1)
delcI_out_ga(x1, x2)  =  delcI_out_ga(x1, x2)
U50_ga(x1, x2, x3)  =  U50_ga(x1, x3)
delcE_in_gga(x1, x2, x3)  =  delcE_in_gga(x1, x2)
delcE_out_gga(x1, x2, x3)  =  delcE_out_gga(x1, x2, x3)
U55_gga(x1, x2, x3)  =  U55_gga(x1, x3)
maxcF_in_gg(x1, x2)  =  maxcF_in_gg(x1, x2)
maxcF_out_gg(x1, x2)  =  maxcF_out_gg(x1, x2)
U51_gg(x1, x2, x3)  =  U51_gg(x1, x2, x3)
U52_gg(x1, x2, x3)  =  U52_gg(x1, x2, x3)
maxcF_in_ga(x1, x2)  =  maxcF_in_ga(x1)
maxcF_out_ga(x1, x2)  =  maxcF_out_ga(x1, x2)
U51_ga(x1, x2, x3)  =  U51_ga(x1, x3)
U52_ga(x1, x2, x3)  =  U52_ga(x1, x3)
delcG_in_gga(x1, x2, x3)  =  delcG_in_gga(x1, x2)
delcG_out_gga(x1, x2, x3)  =  delcG_out_gga(x1, x2, x3)
U56_gga(x1, x2, x3)  =  U56_gga(x1, x3)
delcJ_in_ga(x1, x2)  =  delcJ_in_ga(x1)
delcJ_out_ga(x1, x2)  =  delcJ_out_ga(x1, x2)
U53_ga(x1, x2, x3)  =  U53_ga(x1, x3)
delcH_in_gga(x1, x2, x3)  =  delcH_in_gga(x1, x2)
delcH_out_gga(x1, x2, x3)  =  delcH_out_gga(x1, x2, x3)
U57_gga(x1, x2, x3)  =  U57_gga(x1, x3)
MAXF_IN_GA(x1, x2)  =  MAXF_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(29) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(30) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MAXF_IN_GA(.(f, X1), X2) → MAXF_IN_GA(X1, X2)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
f  =  f
MAXF_IN_GA(x1, x2)  =  MAXF_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(31) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(32) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MAXF_IN_GA(.(f, X1)) → MAXF_IN_GA(X1)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(33) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • MAXF_IN_GA(.(f, X1)) → MAXF_IN_GA(X1)
    The graph contains the following edges 1 > 1

(34) YES

(35) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

U7_GA(X1, X2, delcB_out_ga(X1, X3)) → MAXSORTA_IN_GA(X3, X2)
MAXSORTA_IN_GA(.(X1, []), .(X1, X2)) → U7_GA(X1, X2, delcB_in_ga(X1, X3))
MAXSORTA_IN_GA(.(t, .(t, X1)), .(X2, X3)) → U12_GA(X1, X2, X3, maxcC_in_ga(X1, X2))
U12_GA(X1, X2, X3, maxcC_out_ga(X1, X2)) → U13_GA(X1, X2, X3, delcD_in_gga(X2, X1, X4))
U13_GA(X1, X2, X3, delcD_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4, X3)
MAXSORTA_IN_GA(.(t, .(f, X1)), .(X2, X3)) → U18_GA(X1, X2, X3, maxcC_in_ga(X1, X2))
U18_GA(X1, X2, X3, maxcC_out_ga(X1, X2)) → U19_GA(X1, X2, X3, delcE_in_gga(X2, X1, X4))
U19_GA(X1, X2, X3, delcE_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4, X3)
MAXSORTA_IN_GA(.(f, .(f, X1)), .(X2, X3)) → U24_GA(X1, X2, X3, maxcF_in_ga(X1, X2))
U24_GA(X1, X2, X3, maxcF_out_ga(X1, X2)) → U25_GA(X1, X2, X3, delcG_in_gga(X2, X1, X4))
U25_GA(X1, X2, X3, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4, X3)
MAXSORTA_IN_GA(.(f, .(t, X1)), .(X2, X3)) → U30_GA(X1, X2, X3, maxcC_in_ga(X1, X2))
U30_GA(X1, X2, X3, maxcC_out_ga(X1, X2)) → U31_GA(X1, X2, X3, delcH_in_gga(X2, X1, X4))
U31_GA(X1, X2, X3, delcH_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4, X3)

The TRS R consists of the following rules:

delcB_in_ga(t, []) → delcB_out_ga(t, [])
delcB_in_ga(f, []) → delcB_out_ga(f, [])
maxcC_in_gg([], t) → maxcC_out_gg([], t)
maxcC_in_gg(.(t, X1), X2) → U48_gg(X1, X2, maxcC_in_gg(X1, X2))
maxcC_in_gg(.(f, X1), X2) → U49_gg(X1, X2, maxcC_in_gg(X1, X2))
U49_gg(X1, X2, maxcC_out_gg(X1, X2)) → maxcC_out_gg(.(f, X1), X2)
U48_gg(X1, X2, maxcC_out_gg(X1, X2)) → maxcC_out_gg(.(t, X1), X2)
maxcC_in_ga([], t) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1), X2) → U48_ga(X1, X2, maxcC_in_ga(X1, X2))
maxcC_in_ga(.(f, X1), X2) → U49_ga(X1, X2, maxcC_in_ga(X1, X2))
U49_ga(X1, X2, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, X2, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
delcD_in_gga(t, X1, .(t, X1)) → delcD_out_gga(t, X1, .(t, X1))
delcD_in_gga(f, X1, .(t, .(t, X2))) → U54_gga(X1, X2, delcI_in_ga(X1, X2))
delcI_in_ga([], []) → delcI_out_ga([], [])
delcI_in_ga(.(f, X1), X1) → delcI_out_ga(.(f, X1), X1)
delcI_in_ga(.(t, X1), .(t, X2)) → U50_ga(X1, X2, delcI_in_ga(X1, X2))
U50_ga(X1, X2, delcI_out_ga(X1, X2)) → delcI_out_ga(.(t, X1), .(t, X2))
U54_gga(X1, X2, delcI_out_ga(X1, X2)) → delcD_out_gga(f, X1, .(t, .(t, X2)))
delcE_in_gga(t, X1, .(f, X1)) → delcE_out_gga(t, X1, .(f, X1))
delcE_in_gga(f, X1, .(t, X2)) → U55_gga(X1, X2, delcI_in_ga(.(f, X1), X2))
U55_gga(X1, X2, delcI_out_ga(.(f, X1), X2)) → delcE_out_gga(f, X1, .(t, X2))
maxcF_in_gg([], f) → maxcF_out_gg([], f)
maxcF_in_gg(.(f, X1), X2) → U51_gg(X1, X2, maxcF_in_gg(X1, X2))
maxcF_in_gg(.(t, X1), X2) → U52_gg(X1, X2, maxcC_in_gg(X1, X2))
U52_gg(X1, X2, maxcC_out_gg(X1, X2)) → maxcF_out_gg(.(t, X1), X2)
U51_gg(X1, X2, maxcF_out_gg(X1, X2)) → maxcF_out_gg(.(f, X1), X2)
maxcF_in_ga([], f) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1), X2) → U51_ga(X1, X2, maxcF_in_ga(X1, X2))
maxcF_in_ga(.(t, X1), X2) → U52_ga(X1, X2, maxcC_in_ga(X1, X2))
U52_ga(X1, X2, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U51_ga(X1, X2, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
delcG_in_gga(f, X1, .(f, X1)) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1, .(f, .(f, X2))) → U56_gga(X1, X2, delcJ_in_ga(X1, X2))
delcJ_in_ga([], []) → delcJ_out_ga([], [])
delcJ_in_ga(.(t, X1), X1) → delcJ_out_ga(.(t, X1), X1)
delcJ_in_ga(.(f, X1), .(f, X2)) → U53_ga(X1, X2, delcJ_in_ga(X1, X2))
U53_ga(X1, X2, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))
U56_gga(X1, X2, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
delcH_in_gga(f, X1, .(t, X1)) → delcH_out_gga(f, X1, .(t, X1))
delcH_in_gga(t, X1, .(f, X2)) → U57_gga(X1, X2, delcJ_in_ga(.(t, X1), X2))
U57_gga(X1, X2, delcJ_out_ga(.(t, X1), X2)) → delcH_out_gga(t, X1, .(f, X2))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
[]  =  []
delcB_in_ga(x1, x2)  =  delcB_in_ga(x1)
t  =  t
delcB_out_ga(x1, x2)  =  delcB_out_ga(x1, x2)
f  =  f
maxcC_in_gg(x1, x2)  =  maxcC_in_gg(x1, x2)
maxcC_out_gg(x1, x2)  =  maxcC_out_gg(x1, x2)
U48_gg(x1, x2, x3)  =  U48_gg(x1, x2, x3)
U49_gg(x1, x2, x3)  =  U49_gg(x1, x2, x3)
maxcC_in_ga(x1, x2)  =  maxcC_in_ga(x1)
maxcC_out_ga(x1, x2)  =  maxcC_out_ga(x1, x2)
U48_ga(x1, x2, x3)  =  U48_ga(x1, x3)
U49_ga(x1, x2, x3)  =  U49_ga(x1, x3)
delcD_in_gga(x1, x2, x3)  =  delcD_in_gga(x1, x2)
delcD_out_gga(x1, x2, x3)  =  delcD_out_gga(x1, x2, x3)
U54_gga(x1, x2, x3)  =  U54_gga(x1, x3)
delcI_in_ga(x1, x2)  =  delcI_in_ga(x1)
delcI_out_ga(x1, x2)  =  delcI_out_ga(x1, x2)
U50_ga(x1, x2, x3)  =  U50_ga(x1, x3)
delcE_in_gga(x1, x2, x3)  =  delcE_in_gga(x1, x2)
delcE_out_gga(x1, x2, x3)  =  delcE_out_gga(x1, x2, x3)
U55_gga(x1, x2, x3)  =  U55_gga(x1, x3)
maxcF_in_gg(x1, x2)  =  maxcF_in_gg(x1, x2)
maxcF_out_gg(x1, x2)  =  maxcF_out_gg(x1, x2)
U51_gg(x1, x2, x3)  =  U51_gg(x1, x2, x3)
U52_gg(x1, x2, x3)  =  U52_gg(x1, x2, x3)
maxcF_in_ga(x1, x2)  =  maxcF_in_ga(x1)
maxcF_out_ga(x1, x2)  =  maxcF_out_ga(x1, x2)
U51_ga(x1, x2, x3)  =  U51_ga(x1, x3)
U52_ga(x1, x2, x3)  =  U52_ga(x1, x3)
delcG_in_gga(x1, x2, x3)  =  delcG_in_gga(x1, x2)
delcG_out_gga(x1, x2, x3)  =  delcG_out_gga(x1, x2, x3)
U56_gga(x1, x2, x3)  =  U56_gga(x1, x3)
delcJ_in_ga(x1, x2)  =  delcJ_in_ga(x1)
delcJ_out_ga(x1, x2)  =  delcJ_out_ga(x1, x2)
U53_ga(x1, x2, x3)  =  U53_ga(x1, x3)
delcH_in_gga(x1, x2, x3)  =  delcH_in_gga(x1, x2)
delcH_out_gga(x1, x2, x3)  =  delcH_out_gga(x1, x2, x3)
U57_gga(x1, x2, x3)  =  U57_gga(x1, x3)
MAXSORTA_IN_GA(x1, x2)  =  MAXSORTA_IN_GA(x1)
U7_GA(x1, x2, x3)  =  U7_GA(x1, x3)
U12_GA(x1, x2, x3, x4)  =  U12_GA(x1, x4)
U13_GA(x1, x2, x3, x4)  =  U13_GA(x1, x4)
U18_GA(x1, x2, x3, x4)  =  U18_GA(x1, x4)
U19_GA(x1, x2, x3, x4)  =  U19_GA(x1, x4)
U24_GA(x1, x2, x3, x4)  =  U24_GA(x1, x4)
U25_GA(x1, x2, x3, x4)  =  U25_GA(x1, x4)
U30_GA(x1, x2, x3, x4)  =  U30_GA(x1, x4)
U31_GA(x1, x2, x3, x4)  =  U31_GA(x1, x4)

We have to consider all (P,R,Pi)-chains

(36) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(37) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

U7_GA(X1, X2, delcB_out_ga(X1, X3)) → MAXSORTA_IN_GA(X3, X2)
MAXSORTA_IN_GA(.(X1, []), .(X1, X2)) → U7_GA(X1, X2, delcB_in_ga(X1, X3))
MAXSORTA_IN_GA(.(t, .(t, X1)), .(X2, X3)) → U12_GA(X1, X2, X3, maxcC_in_ga(X1, X2))
U12_GA(X1, X2, X3, maxcC_out_ga(X1, X2)) → U13_GA(X1, X2, X3, delcD_in_gga(X2, X1, X4))
U13_GA(X1, X2, X3, delcD_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4, X3)
MAXSORTA_IN_GA(.(t, .(f, X1)), .(X2, X3)) → U18_GA(X1, X2, X3, maxcC_in_ga(X1, X2))
U18_GA(X1, X2, X3, maxcC_out_ga(X1, X2)) → U19_GA(X1, X2, X3, delcE_in_gga(X2, X1, X4))
U19_GA(X1, X2, X3, delcE_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4, X3)
MAXSORTA_IN_GA(.(f, .(f, X1)), .(X2, X3)) → U24_GA(X1, X2, X3, maxcF_in_ga(X1, X2))
U24_GA(X1, X2, X3, maxcF_out_ga(X1, X2)) → U25_GA(X1, X2, X3, delcG_in_gga(X2, X1, X4))
U25_GA(X1, X2, X3, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4, X3)
MAXSORTA_IN_GA(.(f, .(t, X1)), .(X2, X3)) → U30_GA(X1, X2, X3, maxcC_in_ga(X1, X2))
U30_GA(X1, X2, X3, maxcC_out_ga(X1, X2)) → U31_GA(X1, X2, X3, delcH_in_gga(X2, X1, X4))
U31_GA(X1, X2, X3, delcH_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4, X3)

The TRS R consists of the following rules:

delcB_in_ga(t, []) → delcB_out_ga(t, [])
delcB_in_ga(f, []) → delcB_out_ga(f, [])
maxcC_in_ga([], t) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1), X2) → U48_ga(X1, X2, maxcC_in_ga(X1, X2))
maxcC_in_ga(.(f, X1), X2) → U49_ga(X1, X2, maxcC_in_ga(X1, X2))
delcD_in_gga(t, X1, .(t, X1)) → delcD_out_gga(t, X1, .(t, X1))
delcD_in_gga(f, X1, .(t, .(t, X2))) → U54_gga(X1, X2, delcI_in_ga(X1, X2))
delcE_in_gga(t, X1, .(f, X1)) → delcE_out_gga(t, X1, .(f, X1))
delcE_in_gga(f, X1, .(t, X2)) → U55_gga(X1, X2, delcI_in_ga(.(f, X1), X2))
maxcF_in_ga([], f) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1), X2) → U51_ga(X1, X2, maxcF_in_ga(X1, X2))
maxcF_in_ga(.(t, X1), X2) → U52_ga(X1, X2, maxcC_in_ga(X1, X2))
delcG_in_gga(f, X1, .(f, X1)) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1, .(f, .(f, X2))) → U56_gga(X1, X2, delcJ_in_ga(X1, X2))
delcH_in_gga(f, X1, .(t, X1)) → delcH_out_gga(f, X1, .(t, X1))
delcH_in_gga(t, X1, .(f, X2)) → U57_gga(X1, X2, delcJ_in_ga(.(t, X1), X2))
U48_ga(X1, X2, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
U49_ga(X1, X2, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U54_gga(X1, X2, delcI_out_ga(X1, X2)) → delcD_out_gga(f, X1, .(t, .(t, X2)))
U55_gga(X1, X2, delcI_out_ga(.(f, X1), X2)) → delcE_out_gga(f, X1, .(t, X2))
U51_ga(X1, X2, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
U52_ga(X1, X2, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U56_gga(X1, X2, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
U57_gga(X1, X2, delcJ_out_ga(.(t, X1), X2)) → delcH_out_gga(t, X1, .(f, X2))
delcI_in_ga([], []) → delcI_out_ga([], [])
delcI_in_ga(.(f, X1), X1) → delcI_out_ga(.(f, X1), X1)
delcI_in_ga(.(t, X1), .(t, X2)) → U50_ga(X1, X2, delcI_in_ga(X1, X2))
delcJ_in_ga([], []) → delcJ_out_ga([], [])
delcJ_in_ga(.(t, X1), X1) → delcJ_out_ga(.(t, X1), X1)
delcJ_in_ga(.(f, X1), .(f, X2)) → U53_ga(X1, X2, delcJ_in_ga(X1, X2))
U50_ga(X1, X2, delcI_out_ga(X1, X2)) → delcI_out_ga(.(t, X1), .(t, X2))
U53_ga(X1, X2, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
[]  =  []
delcB_in_ga(x1, x2)  =  delcB_in_ga(x1)
t  =  t
delcB_out_ga(x1, x2)  =  delcB_out_ga(x1, x2)
f  =  f
maxcC_in_ga(x1, x2)  =  maxcC_in_ga(x1)
maxcC_out_ga(x1, x2)  =  maxcC_out_ga(x1, x2)
U48_ga(x1, x2, x3)  =  U48_ga(x1, x3)
U49_ga(x1, x2, x3)  =  U49_ga(x1, x3)
delcD_in_gga(x1, x2, x3)  =  delcD_in_gga(x1, x2)
delcD_out_gga(x1, x2, x3)  =  delcD_out_gga(x1, x2, x3)
U54_gga(x1, x2, x3)  =  U54_gga(x1, x3)
delcI_in_ga(x1, x2)  =  delcI_in_ga(x1)
delcI_out_ga(x1, x2)  =  delcI_out_ga(x1, x2)
U50_ga(x1, x2, x3)  =  U50_ga(x1, x3)
delcE_in_gga(x1, x2, x3)  =  delcE_in_gga(x1, x2)
delcE_out_gga(x1, x2, x3)  =  delcE_out_gga(x1, x2, x3)
U55_gga(x1, x2, x3)  =  U55_gga(x1, x3)
maxcF_in_ga(x1, x2)  =  maxcF_in_ga(x1)
maxcF_out_ga(x1, x2)  =  maxcF_out_ga(x1, x2)
U51_ga(x1, x2, x3)  =  U51_ga(x1, x3)
U52_ga(x1, x2, x3)  =  U52_ga(x1, x3)
delcG_in_gga(x1, x2, x3)  =  delcG_in_gga(x1, x2)
delcG_out_gga(x1, x2, x3)  =  delcG_out_gga(x1, x2, x3)
U56_gga(x1, x2, x3)  =  U56_gga(x1, x3)
delcJ_in_ga(x1, x2)  =  delcJ_in_ga(x1)
delcJ_out_ga(x1, x2)  =  delcJ_out_ga(x1, x2)
U53_ga(x1, x2, x3)  =  U53_ga(x1, x3)
delcH_in_gga(x1, x2, x3)  =  delcH_in_gga(x1, x2)
delcH_out_gga(x1, x2, x3)  =  delcH_out_gga(x1, x2, x3)
U57_gga(x1, x2, x3)  =  U57_gga(x1, x3)
MAXSORTA_IN_GA(x1, x2)  =  MAXSORTA_IN_GA(x1)
U7_GA(x1, x2, x3)  =  U7_GA(x1, x3)
U12_GA(x1, x2, x3, x4)  =  U12_GA(x1, x4)
U13_GA(x1, x2, x3, x4)  =  U13_GA(x1, x4)
U18_GA(x1, x2, x3, x4)  =  U18_GA(x1, x4)
U19_GA(x1, x2, x3, x4)  =  U19_GA(x1, x4)
U24_GA(x1, x2, x3, x4)  =  U24_GA(x1, x4)
U25_GA(x1, x2, x3, x4)  =  U25_GA(x1, x4)
U30_GA(x1, x2, x3, x4)  =  U30_GA(x1, x4)
U31_GA(x1, x2, x3, x4)  =  U31_GA(x1, x4)

We have to consider all (P,R,Pi)-chains

(38) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(39) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U7_GA(X1, delcB_out_ga(X1, X3)) → MAXSORTA_IN_GA(X3)
MAXSORTA_IN_GA(.(X1, [])) → U7_GA(X1, delcB_in_ga(X1))
MAXSORTA_IN_GA(.(t, .(t, X1))) → U12_GA(X1, maxcC_in_ga(X1))
U12_GA(X1, maxcC_out_ga(X1, X2)) → U13_GA(X1, delcD_in_gga(X2, X1))
U13_GA(X1, delcD_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(t, .(f, X1))) → U18_GA(X1, maxcC_in_ga(X1))
U18_GA(X1, maxcC_out_ga(X1, X2)) → U19_GA(X1, delcE_in_gga(X2, X1))
U19_GA(X1, delcE_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(f, X1))) → U24_GA(X1, maxcF_in_ga(X1))
U24_GA(X1, maxcF_out_ga(X1, X2)) → U25_GA(X1, delcG_in_gga(X2, X1))
U25_GA(X1, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(t, X1))) → U30_GA(X1, maxcC_in_ga(X1))
U30_GA(X1, maxcC_out_ga(X1, X2)) → U31_GA(X1, delcH_in_gga(X2, X1))
U31_GA(X1, delcH_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)

The TRS R consists of the following rules:

delcB_in_ga(t) → delcB_out_ga(t, [])
delcB_in_ga(f) → delcB_out_ga(f, [])
maxcC_in_ga([]) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1)) → U48_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga(.(f, X1)) → U49_ga(X1, maxcC_in_ga(X1))
delcD_in_gga(t, X1) → delcD_out_gga(t, X1, .(t, X1))
delcD_in_gga(f, X1) → U54_gga(X1, delcI_in_ga(X1))
delcE_in_gga(t, X1) → delcE_out_gga(t, X1, .(f, X1))
delcE_in_gga(f, X1) → U55_gga(X1, delcI_in_ga(.(f, X1)))
maxcF_in_ga([]) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1)) → U51_ga(X1, maxcF_in_ga(X1))
maxcF_in_ga(.(t, X1)) → U52_ga(X1, maxcC_in_ga(X1))
delcG_in_gga(f, X1) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1) → U56_gga(X1, delcJ_in_ga(X1))
delcH_in_gga(f, X1) → delcH_out_gga(f, X1, .(t, X1))
delcH_in_gga(t, X1) → U57_gga(X1, delcJ_in_ga(.(t, X1)))
U48_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
U49_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U54_gga(X1, delcI_out_ga(X1, X2)) → delcD_out_gga(f, X1, .(t, .(t, X2)))
U55_gga(X1, delcI_out_ga(.(f, X1), X2)) → delcE_out_gga(f, X1, .(t, X2))
U51_ga(X1, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
U52_ga(X1, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U56_gga(X1, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
U57_gga(X1, delcJ_out_ga(.(t, X1), X2)) → delcH_out_gga(t, X1, .(f, X2))
delcI_in_ga([]) → delcI_out_ga([], [])
delcI_in_ga(.(f, X1)) → delcI_out_ga(.(f, X1), X1)
delcI_in_ga(.(t, X1)) → U50_ga(X1, delcI_in_ga(X1))
delcJ_in_ga([]) → delcJ_out_ga([], [])
delcJ_in_ga(.(t, X1)) → delcJ_out_ga(.(t, X1), X1)
delcJ_in_ga(.(f, X1)) → U53_ga(X1, delcJ_in_ga(X1))
U50_ga(X1, delcI_out_ga(X1, X2)) → delcI_out_ga(.(t, X1), .(t, X2))
U53_ga(X1, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))

The set Q consists of the following terms:

delcB_in_ga(x0)
maxcC_in_ga(x0)
delcD_in_gga(x0, x1)
delcE_in_gga(x0, x1)
maxcF_in_ga(x0)
delcG_in_gga(x0, x1)
delcH_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U54_gga(x0, x1)
U55_gga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
U57_gga(x0, x1)
delcI_in_ga(x0)
delcJ_in_ga(x0)
U50_ga(x0, x1)
U53_ga(x0, x1)

We have to consider all (P,Q,R)-chains.

(40) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule MAXSORTA_IN_GA(.(X1, [])) → U7_GA(X1, delcB_in_ga(X1)) at position [1] we obtained the following new rules [LPAR04]:

MAXSORTA_IN_GA(.(t, [])) → U7_GA(t, delcB_out_ga(t, []))
MAXSORTA_IN_GA(.(f, [])) → U7_GA(f, delcB_out_ga(f, []))

(41) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U7_GA(X1, delcB_out_ga(X1, X3)) → MAXSORTA_IN_GA(X3)
MAXSORTA_IN_GA(.(t, .(t, X1))) → U12_GA(X1, maxcC_in_ga(X1))
U12_GA(X1, maxcC_out_ga(X1, X2)) → U13_GA(X1, delcD_in_gga(X2, X1))
U13_GA(X1, delcD_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(t, .(f, X1))) → U18_GA(X1, maxcC_in_ga(X1))
U18_GA(X1, maxcC_out_ga(X1, X2)) → U19_GA(X1, delcE_in_gga(X2, X1))
U19_GA(X1, delcE_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(f, X1))) → U24_GA(X1, maxcF_in_ga(X1))
U24_GA(X1, maxcF_out_ga(X1, X2)) → U25_GA(X1, delcG_in_gga(X2, X1))
U25_GA(X1, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(t, X1))) → U30_GA(X1, maxcC_in_ga(X1))
U30_GA(X1, maxcC_out_ga(X1, X2)) → U31_GA(X1, delcH_in_gga(X2, X1))
U31_GA(X1, delcH_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(t, [])) → U7_GA(t, delcB_out_ga(t, []))
MAXSORTA_IN_GA(.(f, [])) → U7_GA(f, delcB_out_ga(f, []))

The TRS R consists of the following rules:

delcB_in_ga(t) → delcB_out_ga(t, [])
delcB_in_ga(f) → delcB_out_ga(f, [])
maxcC_in_ga([]) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1)) → U48_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga(.(f, X1)) → U49_ga(X1, maxcC_in_ga(X1))
delcD_in_gga(t, X1) → delcD_out_gga(t, X1, .(t, X1))
delcD_in_gga(f, X1) → U54_gga(X1, delcI_in_ga(X1))
delcE_in_gga(t, X1) → delcE_out_gga(t, X1, .(f, X1))
delcE_in_gga(f, X1) → U55_gga(X1, delcI_in_ga(.(f, X1)))
maxcF_in_ga([]) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1)) → U51_ga(X1, maxcF_in_ga(X1))
maxcF_in_ga(.(t, X1)) → U52_ga(X1, maxcC_in_ga(X1))
delcG_in_gga(f, X1) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1) → U56_gga(X1, delcJ_in_ga(X1))
delcH_in_gga(f, X1) → delcH_out_gga(f, X1, .(t, X1))
delcH_in_gga(t, X1) → U57_gga(X1, delcJ_in_ga(.(t, X1)))
U48_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
U49_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U54_gga(X1, delcI_out_ga(X1, X2)) → delcD_out_gga(f, X1, .(t, .(t, X2)))
U55_gga(X1, delcI_out_ga(.(f, X1), X2)) → delcE_out_gga(f, X1, .(t, X2))
U51_ga(X1, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
U52_ga(X1, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U56_gga(X1, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
U57_gga(X1, delcJ_out_ga(.(t, X1), X2)) → delcH_out_gga(t, X1, .(f, X2))
delcI_in_ga([]) → delcI_out_ga([], [])
delcI_in_ga(.(f, X1)) → delcI_out_ga(.(f, X1), X1)
delcI_in_ga(.(t, X1)) → U50_ga(X1, delcI_in_ga(X1))
delcJ_in_ga([]) → delcJ_out_ga([], [])
delcJ_in_ga(.(t, X1)) → delcJ_out_ga(.(t, X1), X1)
delcJ_in_ga(.(f, X1)) → U53_ga(X1, delcJ_in_ga(X1))
U50_ga(X1, delcI_out_ga(X1, X2)) → delcI_out_ga(.(t, X1), .(t, X2))
U53_ga(X1, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))

The set Q consists of the following terms:

delcB_in_ga(x0)
maxcC_in_ga(x0)
delcD_in_gga(x0, x1)
delcE_in_gga(x0, x1)
maxcF_in_ga(x0)
delcG_in_gga(x0, x1)
delcH_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U54_gga(x0, x1)
U55_gga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
U57_gga(x0, x1)
delcI_in_ga(x0)
delcJ_in_ga(x0)
U50_ga(x0, x1)
U53_ga(x0, x1)

We have to consider all (P,Q,R)-chains.

(42) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(43) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U7_GA(X1, delcB_out_ga(X1, X3)) → MAXSORTA_IN_GA(X3)
MAXSORTA_IN_GA(.(t, .(t, X1))) → U12_GA(X1, maxcC_in_ga(X1))
U12_GA(X1, maxcC_out_ga(X1, X2)) → U13_GA(X1, delcD_in_gga(X2, X1))
U13_GA(X1, delcD_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(t, .(f, X1))) → U18_GA(X1, maxcC_in_ga(X1))
U18_GA(X1, maxcC_out_ga(X1, X2)) → U19_GA(X1, delcE_in_gga(X2, X1))
U19_GA(X1, delcE_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(f, X1))) → U24_GA(X1, maxcF_in_ga(X1))
U24_GA(X1, maxcF_out_ga(X1, X2)) → U25_GA(X1, delcG_in_gga(X2, X1))
U25_GA(X1, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(t, X1))) → U30_GA(X1, maxcC_in_ga(X1))
U30_GA(X1, maxcC_out_ga(X1, X2)) → U31_GA(X1, delcH_in_gga(X2, X1))
U31_GA(X1, delcH_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(t, [])) → U7_GA(t, delcB_out_ga(t, []))
MAXSORTA_IN_GA(.(f, [])) → U7_GA(f, delcB_out_ga(f, []))

The TRS R consists of the following rules:

delcH_in_gga(f, X1) → delcH_out_gga(f, X1, .(t, X1))
delcH_in_gga(t, X1) → U57_gga(X1, delcJ_in_ga(.(t, X1)))
delcJ_in_ga(.(t, X1)) → delcJ_out_ga(.(t, X1), X1)
U57_gga(X1, delcJ_out_ga(.(t, X1), X2)) → delcH_out_gga(t, X1, .(f, X2))
maxcC_in_ga([]) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1)) → U48_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga(.(f, X1)) → U49_ga(X1, maxcC_in_ga(X1))
U49_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
delcG_in_gga(f, X1) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1) → U56_gga(X1, delcJ_in_ga(X1))
delcJ_in_ga([]) → delcJ_out_ga([], [])
delcJ_in_ga(.(f, X1)) → U53_ga(X1, delcJ_in_ga(X1))
U56_gga(X1, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
U53_ga(X1, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))
maxcF_in_ga([]) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1)) → U51_ga(X1, maxcF_in_ga(X1))
maxcF_in_ga(.(t, X1)) → U52_ga(X1, maxcC_in_ga(X1))
U52_ga(X1, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U51_ga(X1, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
delcE_in_gga(t, X1) → delcE_out_gga(t, X1, .(f, X1))
delcE_in_gga(f, X1) → U55_gga(X1, delcI_in_ga(.(f, X1)))
delcI_in_ga(.(f, X1)) → delcI_out_ga(.(f, X1), X1)
U55_gga(X1, delcI_out_ga(.(f, X1), X2)) → delcE_out_gga(f, X1, .(t, X2))
delcD_in_gga(t, X1) → delcD_out_gga(t, X1, .(t, X1))
delcD_in_gga(f, X1) → U54_gga(X1, delcI_in_ga(X1))
delcI_in_ga([]) → delcI_out_ga([], [])
delcI_in_ga(.(t, X1)) → U50_ga(X1, delcI_in_ga(X1))
U54_gga(X1, delcI_out_ga(X1, X2)) → delcD_out_gga(f, X1, .(t, .(t, X2)))
U50_ga(X1, delcI_out_ga(X1, X2)) → delcI_out_ga(.(t, X1), .(t, X2))

The set Q consists of the following terms:

delcB_in_ga(x0)
maxcC_in_ga(x0)
delcD_in_gga(x0, x1)
delcE_in_gga(x0, x1)
maxcF_in_ga(x0)
delcG_in_gga(x0, x1)
delcH_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U54_gga(x0, x1)
U55_gga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
U57_gga(x0, x1)
delcI_in_ga(x0)
delcJ_in_ga(x0)
U50_ga(x0, x1)
U53_ga(x0, x1)

We have to consider all (P,Q,R)-chains.

(44) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

delcB_in_ga(x0)

(45) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U7_GA(X1, delcB_out_ga(X1, X3)) → MAXSORTA_IN_GA(X3)
MAXSORTA_IN_GA(.(t, .(t, X1))) → U12_GA(X1, maxcC_in_ga(X1))
U12_GA(X1, maxcC_out_ga(X1, X2)) → U13_GA(X1, delcD_in_gga(X2, X1))
U13_GA(X1, delcD_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(t, .(f, X1))) → U18_GA(X1, maxcC_in_ga(X1))
U18_GA(X1, maxcC_out_ga(X1, X2)) → U19_GA(X1, delcE_in_gga(X2, X1))
U19_GA(X1, delcE_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(f, X1))) → U24_GA(X1, maxcF_in_ga(X1))
U24_GA(X1, maxcF_out_ga(X1, X2)) → U25_GA(X1, delcG_in_gga(X2, X1))
U25_GA(X1, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(t, X1))) → U30_GA(X1, maxcC_in_ga(X1))
U30_GA(X1, maxcC_out_ga(X1, X2)) → U31_GA(X1, delcH_in_gga(X2, X1))
U31_GA(X1, delcH_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(t, [])) → U7_GA(t, delcB_out_ga(t, []))
MAXSORTA_IN_GA(.(f, [])) → U7_GA(f, delcB_out_ga(f, []))

The TRS R consists of the following rules:

delcH_in_gga(f, X1) → delcH_out_gga(f, X1, .(t, X1))
delcH_in_gga(t, X1) → U57_gga(X1, delcJ_in_ga(.(t, X1)))
delcJ_in_ga(.(t, X1)) → delcJ_out_ga(.(t, X1), X1)
U57_gga(X1, delcJ_out_ga(.(t, X1), X2)) → delcH_out_gga(t, X1, .(f, X2))
maxcC_in_ga([]) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1)) → U48_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga(.(f, X1)) → U49_ga(X1, maxcC_in_ga(X1))
U49_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
delcG_in_gga(f, X1) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1) → U56_gga(X1, delcJ_in_ga(X1))
delcJ_in_ga([]) → delcJ_out_ga([], [])
delcJ_in_ga(.(f, X1)) → U53_ga(X1, delcJ_in_ga(X1))
U56_gga(X1, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
U53_ga(X1, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))
maxcF_in_ga([]) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1)) → U51_ga(X1, maxcF_in_ga(X1))
maxcF_in_ga(.(t, X1)) → U52_ga(X1, maxcC_in_ga(X1))
U52_ga(X1, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U51_ga(X1, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
delcE_in_gga(t, X1) → delcE_out_gga(t, X1, .(f, X1))
delcE_in_gga(f, X1) → U55_gga(X1, delcI_in_ga(.(f, X1)))
delcI_in_ga(.(f, X1)) → delcI_out_ga(.(f, X1), X1)
U55_gga(X1, delcI_out_ga(.(f, X1), X2)) → delcE_out_gga(f, X1, .(t, X2))
delcD_in_gga(t, X1) → delcD_out_gga(t, X1, .(t, X1))
delcD_in_gga(f, X1) → U54_gga(X1, delcI_in_ga(X1))
delcI_in_ga([]) → delcI_out_ga([], [])
delcI_in_ga(.(t, X1)) → U50_ga(X1, delcI_in_ga(X1))
U54_gga(X1, delcI_out_ga(X1, X2)) → delcD_out_gga(f, X1, .(t, .(t, X2)))
U50_ga(X1, delcI_out_ga(X1, X2)) → delcI_out_ga(.(t, X1), .(t, X2))

The set Q consists of the following terms:

maxcC_in_ga(x0)
delcD_in_gga(x0, x1)
delcE_in_gga(x0, x1)
maxcF_in_ga(x0)
delcG_in_gga(x0, x1)
delcH_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U54_gga(x0, x1)
U55_gga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
U57_gga(x0, x1)
delcI_in_ga(x0)
delcJ_in_ga(x0)
U50_ga(x0, x1)
U53_ga(x0, x1)

We have to consider all (P,Q,R)-chains.

(46) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U7_GA(X1, delcB_out_ga(X1, X3)) → MAXSORTA_IN_GA(X3) we obtained the following new rules [LPAR04]:

U7_GA(t, delcB_out_ga(t, [])) → MAXSORTA_IN_GA([])
U7_GA(f, delcB_out_ga(f, [])) → MAXSORTA_IN_GA([])

(47) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MAXSORTA_IN_GA(.(t, .(t, X1))) → U12_GA(X1, maxcC_in_ga(X1))
U12_GA(X1, maxcC_out_ga(X1, X2)) → U13_GA(X1, delcD_in_gga(X2, X1))
U13_GA(X1, delcD_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(t, .(f, X1))) → U18_GA(X1, maxcC_in_ga(X1))
U18_GA(X1, maxcC_out_ga(X1, X2)) → U19_GA(X1, delcE_in_gga(X2, X1))
U19_GA(X1, delcE_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(f, X1))) → U24_GA(X1, maxcF_in_ga(X1))
U24_GA(X1, maxcF_out_ga(X1, X2)) → U25_GA(X1, delcG_in_gga(X2, X1))
U25_GA(X1, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(t, X1))) → U30_GA(X1, maxcC_in_ga(X1))
U30_GA(X1, maxcC_out_ga(X1, X2)) → U31_GA(X1, delcH_in_gga(X2, X1))
U31_GA(X1, delcH_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(t, [])) → U7_GA(t, delcB_out_ga(t, []))
MAXSORTA_IN_GA(.(f, [])) → U7_GA(f, delcB_out_ga(f, []))
U7_GA(t, delcB_out_ga(t, [])) → MAXSORTA_IN_GA([])
U7_GA(f, delcB_out_ga(f, [])) → MAXSORTA_IN_GA([])

The TRS R consists of the following rules:

delcH_in_gga(f, X1) → delcH_out_gga(f, X1, .(t, X1))
delcH_in_gga(t, X1) → U57_gga(X1, delcJ_in_ga(.(t, X1)))
delcJ_in_ga(.(t, X1)) → delcJ_out_ga(.(t, X1), X1)
U57_gga(X1, delcJ_out_ga(.(t, X1), X2)) → delcH_out_gga(t, X1, .(f, X2))
maxcC_in_ga([]) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1)) → U48_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga(.(f, X1)) → U49_ga(X1, maxcC_in_ga(X1))
U49_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
delcG_in_gga(f, X1) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1) → U56_gga(X1, delcJ_in_ga(X1))
delcJ_in_ga([]) → delcJ_out_ga([], [])
delcJ_in_ga(.(f, X1)) → U53_ga(X1, delcJ_in_ga(X1))
U56_gga(X1, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
U53_ga(X1, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))
maxcF_in_ga([]) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1)) → U51_ga(X1, maxcF_in_ga(X1))
maxcF_in_ga(.(t, X1)) → U52_ga(X1, maxcC_in_ga(X1))
U52_ga(X1, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U51_ga(X1, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
delcE_in_gga(t, X1) → delcE_out_gga(t, X1, .(f, X1))
delcE_in_gga(f, X1) → U55_gga(X1, delcI_in_ga(.(f, X1)))
delcI_in_ga(.(f, X1)) → delcI_out_ga(.(f, X1), X1)
U55_gga(X1, delcI_out_ga(.(f, X1), X2)) → delcE_out_gga(f, X1, .(t, X2))
delcD_in_gga(t, X1) → delcD_out_gga(t, X1, .(t, X1))
delcD_in_gga(f, X1) → U54_gga(X1, delcI_in_ga(X1))
delcI_in_ga([]) → delcI_out_ga([], [])
delcI_in_ga(.(t, X1)) → U50_ga(X1, delcI_in_ga(X1))
U54_gga(X1, delcI_out_ga(X1, X2)) → delcD_out_gga(f, X1, .(t, .(t, X2)))
U50_ga(X1, delcI_out_ga(X1, X2)) → delcI_out_ga(.(t, X1), .(t, X2))

The set Q consists of the following terms:

maxcC_in_ga(x0)
delcD_in_gga(x0, x1)
delcE_in_gga(x0, x1)
maxcF_in_ga(x0)
delcG_in_gga(x0, x1)
delcH_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U54_gga(x0, x1)
U55_gga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
U57_gga(x0, x1)
delcI_in_ga(x0)
delcJ_in_ga(x0)
U50_ga(x0, x1)
U53_ga(x0, x1)

We have to consider all (P,Q,R)-chains.

(48) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 4 less nodes.

(49) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U12_GA(X1, maxcC_out_ga(X1, X2)) → U13_GA(X1, delcD_in_gga(X2, X1))
U13_GA(X1, delcD_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(t, .(t, X1))) → U12_GA(X1, maxcC_in_ga(X1))
MAXSORTA_IN_GA(.(t, .(f, X1))) → U18_GA(X1, maxcC_in_ga(X1))
U18_GA(X1, maxcC_out_ga(X1, X2)) → U19_GA(X1, delcE_in_gga(X2, X1))
U19_GA(X1, delcE_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(f, X1))) → U24_GA(X1, maxcF_in_ga(X1))
U24_GA(X1, maxcF_out_ga(X1, X2)) → U25_GA(X1, delcG_in_gga(X2, X1))
U25_GA(X1, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(t, X1))) → U30_GA(X1, maxcC_in_ga(X1))
U30_GA(X1, maxcC_out_ga(X1, X2)) → U31_GA(X1, delcH_in_gga(X2, X1))
U31_GA(X1, delcH_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)

The TRS R consists of the following rules:

delcH_in_gga(f, X1) → delcH_out_gga(f, X1, .(t, X1))
delcH_in_gga(t, X1) → U57_gga(X1, delcJ_in_ga(.(t, X1)))
delcJ_in_ga(.(t, X1)) → delcJ_out_ga(.(t, X1), X1)
U57_gga(X1, delcJ_out_ga(.(t, X1), X2)) → delcH_out_gga(t, X1, .(f, X2))
maxcC_in_ga([]) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1)) → U48_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga(.(f, X1)) → U49_ga(X1, maxcC_in_ga(X1))
U49_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
delcG_in_gga(f, X1) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1) → U56_gga(X1, delcJ_in_ga(X1))
delcJ_in_ga([]) → delcJ_out_ga([], [])
delcJ_in_ga(.(f, X1)) → U53_ga(X1, delcJ_in_ga(X1))
U56_gga(X1, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
U53_ga(X1, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))
maxcF_in_ga([]) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1)) → U51_ga(X1, maxcF_in_ga(X1))
maxcF_in_ga(.(t, X1)) → U52_ga(X1, maxcC_in_ga(X1))
U52_ga(X1, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U51_ga(X1, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
delcE_in_gga(t, X1) → delcE_out_gga(t, X1, .(f, X1))
delcE_in_gga(f, X1) → U55_gga(X1, delcI_in_ga(.(f, X1)))
delcI_in_ga(.(f, X1)) → delcI_out_ga(.(f, X1), X1)
U55_gga(X1, delcI_out_ga(.(f, X1), X2)) → delcE_out_gga(f, X1, .(t, X2))
delcD_in_gga(t, X1) → delcD_out_gga(t, X1, .(t, X1))
delcD_in_gga(f, X1) → U54_gga(X1, delcI_in_ga(X1))
delcI_in_ga([]) → delcI_out_ga([], [])
delcI_in_ga(.(t, X1)) → U50_ga(X1, delcI_in_ga(X1))
U54_gga(X1, delcI_out_ga(X1, X2)) → delcD_out_gga(f, X1, .(t, .(t, X2)))
U50_ga(X1, delcI_out_ga(X1, X2)) → delcI_out_ga(.(t, X1), .(t, X2))

The set Q consists of the following terms:

maxcC_in_ga(x0)
delcD_in_gga(x0, x1)
delcE_in_gga(x0, x1)
maxcF_in_ga(x0)
delcG_in_gga(x0, x1)
delcH_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U54_gga(x0, x1)
U55_gga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
U57_gga(x0, x1)
delcI_in_ga(x0)
delcJ_in_ga(x0)
U50_ga(x0, x1)
U53_ga(x0, x1)

We have to consider all (P,Q,R)-chains.

(50) QDPQMonotonicMRRProof (EQUIVALENT transformation)

By using the Q-monotonic rule removal processor with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented such that it always occurs at a strongly monotonic position in a (P,Q,R)-chain.

Strictly oriented rules of the TRS R:

delcH_in_gga(f, X1) → delcH_out_gga(f, X1, .(t, X1))

Used ordering: Polynomial interpretation [POLO]:

POL(.(x1, x2)) = 0   
POL(MAXSORTA_IN_GA(x1)) = 0   
POL(U12_GA(x1, x2)) = 2·x2   
POL(U13_GA(x1, x2)) = 0   
POL(U18_GA(x1, x2)) = 0   
POL(U19_GA(x1, x2)) = 0   
POL(U24_GA(x1, x2)) = 0   
POL(U25_GA(x1, x2)) = 0   
POL(U30_GA(x1, x2)) = 2·x2   
POL(U31_GA(x1, x2)) = x2   
POL(U48_ga(x1, x2)) = x2   
POL(U49_ga(x1, x2)) = 2·x2   
POL(U50_ga(x1, x2)) = 0   
POL(U51_ga(x1, x2)) = 0   
POL(U52_ga(x1, x2)) = 0   
POL(U53_ga(x1, x2)) = 2·x2   
POL(U54_gga(x1, x2)) = 0   
POL(U55_gga(x1, x2)) = x1   
POL(U56_gga(x1, x2)) = 1 + x1   
POL(U57_gga(x1, x2)) = 0   
POL([]) = 0   
POL(delcD_in_gga(x1, x2)) = 2·x1   
POL(delcD_out_gga(x1, x2, x3)) = 0   
POL(delcE_in_gga(x1, x2)) = x2   
POL(delcE_out_gga(x1, x2, x3)) = x2   
POL(delcG_in_gga(x1, x2)) = 2 + x2   
POL(delcG_out_gga(x1, x2, x3)) = 1   
POL(delcH_in_gga(x1, x2)) = x1   
POL(delcH_out_gga(x1, x2, x3)) = 0   
POL(delcI_in_ga(x1)) = 0   
POL(delcI_out_ga(x1, x2)) = 0   
POL(delcJ_in_ga(x1)) = 0   
POL(delcJ_out_ga(x1, x2)) = 0   
POL(f) = 2   
POL(maxcC_in_ga(x1)) = 0   
POL(maxcC_out_ga(x1, x2)) = 2·x1 + 2·x2   
POL(maxcF_in_ga(x1)) = 0   
POL(maxcF_out_ga(x1, x2)) = 0   
POL(t) = 0   

(51) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U12_GA(X1, maxcC_out_ga(X1, X2)) → U13_GA(X1, delcD_in_gga(X2, X1))
U13_GA(X1, delcD_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(t, .(t, X1))) → U12_GA(X1, maxcC_in_ga(X1))
MAXSORTA_IN_GA(.(t, .(f, X1))) → U18_GA(X1, maxcC_in_ga(X1))
U18_GA(X1, maxcC_out_ga(X1, X2)) → U19_GA(X1, delcE_in_gga(X2, X1))
U19_GA(X1, delcE_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(f, X1))) → U24_GA(X1, maxcF_in_ga(X1))
U24_GA(X1, maxcF_out_ga(X1, X2)) → U25_GA(X1, delcG_in_gga(X2, X1))
U25_GA(X1, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(t, X1))) → U30_GA(X1, maxcC_in_ga(X1))
U30_GA(X1, maxcC_out_ga(X1, X2)) → U31_GA(X1, delcH_in_gga(X2, X1))
U31_GA(X1, delcH_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)

The TRS R consists of the following rules:

delcH_in_gga(t, X1) → U57_gga(X1, delcJ_in_ga(.(t, X1)))
delcJ_in_ga(.(t, X1)) → delcJ_out_ga(.(t, X1), X1)
U57_gga(X1, delcJ_out_ga(.(t, X1), X2)) → delcH_out_gga(t, X1, .(f, X2))
maxcC_in_ga([]) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1)) → U48_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga(.(f, X1)) → U49_ga(X1, maxcC_in_ga(X1))
U49_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
delcG_in_gga(f, X1) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1) → U56_gga(X1, delcJ_in_ga(X1))
delcJ_in_ga([]) → delcJ_out_ga([], [])
delcJ_in_ga(.(f, X1)) → U53_ga(X1, delcJ_in_ga(X1))
U56_gga(X1, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
U53_ga(X1, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))
maxcF_in_ga([]) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1)) → U51_ga(X1, maxcF_in_ga(X1))
maxcF_in_ga(.(t, X1)) → U52_ga(X1, maxcC_in_ga(X1))
U52_ga(X1, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U51_ga(X1, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
delcE_in_gga(t, X1) → delcE_out_gga(t, X1, .(f, X1))
delcE_in_gga(f, X1) → U55_gga(X1, delcI_in_ga(.(f, X1)))
delcI_in_ga(.(f, X1)) → delcI_out_ga(.(f, X1), X1)
U55_gga(X1, delcI_out_ga(.(f, X1), X2)) → delcE_out_gga(f, X1, .(t, X2))
delcD_in_gga(t, X1) → delcD_out_gga(t, X1, .(t, X1))
delcD_in_gga(f, X1) → U54_gga(X1, delcI_in_ga(X1))
delcI_in_ga([]) → delcI_out_ga([], [])
delcI_in_ga(.(t, X1)) → U50_ga(X1, delcI_in_ga(X1))
U54_gga(X1, delcI_out_ga(X1, X2)) → delcD_out_gga(f, X1, .(t, .(t, X2)))
U50_ga(X1, delcI_out_ga(X1, X2)) → delcI_out_ga(.(t, X1), .(t, X2))

The set Q consists of the following terms:

maxcC_in_ga(x0)
delcD_in_gga(x0, x1)
delcE_in_gga(x0, x1)
maxcF_in_ga(x0)
delcG_in_gga(x0, x1)
delcH_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U54_gga(x0, x1)
U55_gga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
U57_gga(x0, x1)
delcI_in_ga(x0)
delcJ_in_ga(x0)
U50_ga(x0, x1)
U53_ga(x0, x1)

We have to consider all (P,Q,R)-chains.

(52) QDPQMonotonicMRRProof (EQUIVALENT transformation)

By using the Q-monotonic rule removal processor with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented such that it always occurs at a strongly monotonic position in a (P,Q,R)-chain.

Strictly oriented rules of the TRS R:

U55_gga(X1, delcI_out_ga(.(f, X1), X2)) → delcE_out_gga(f, X1, .(t, X2))

Used ordering: Polynomial interpretation [POLO]:

POL(.(x1, x2)) = 0   
POL(MAXSORTA_IN_GA(x1)) = 0   
POL(U12_GA(x1, x2)) = 0   
POL(U13_GA(x1, x2)) = 0   
POL(U18_GA(x1, x2)) = 2·x2   
POL(U19_GA(x1, x2)) = x2   
POL(U24_GA(x1, x2)) = 0   
POL(U25_GA(x1, x2)) = 0   
POL(U30_GA(x1, x2)) = 0   
POL(U31_GA(x1, x2)) = 0   
POL(U48_ga(x1, x2)) = x2   
POL(U49_ga(x1, x2)) = x2   
POL(U50_ga(x1, x2)) = 2   
POL(U51_ga(x1, x2)) = 0   
POL(U52_ga(x1, x2)) = 0   
POL(U53_ga(x1, x2)) = 0   
POL(U54_gga(x1, x2)) = x1   
POL(U55_gga(x1, x2)) = 2·x2   
POL(U56_gga(x1, x2)) = x1   
POL(U57_gga(x1, x2)) = 1   
POL([]) = 0   
POL(delcD_in_gga(x1, x2)) = 2·x2   
POL(delcD_out_gga(x1, x2, x3)) = x3   
POL(delcE_in_gga(x1, x2)) = 2·x1   
POL(delcE_out_gga(x1, x2, x3)) = 2·x3   
POL(delcG_in_gga(x1, x2)) = 2 + 2·x2   
POL(delcG_out_gga(x1, x2, x3)) = x3   
POL(delcH_in_gga(x1, x2)) = 1   
POL(delcH_out_gga(x1, x2, x3)) = 0   
POL(delcI_in_ga(x1)) = 2   
POL(delcI_out_ga(x1, x2)) = 1   
POL(delcJ_in_ga(x1)) = 1   
POL(delcJ_out_ga(x1, x2)) = 0   
POL(f) = 2   
POL(maxcC_in_ga(x1)) = 0   
POL(maxcC_out_ga(x1, x2)) = x2   
POL(maxcF_in_ga(x1)) = 0   
POL(maxcF_out_ga(x1, x2)) = 0   
POL(t) = 0   

(53) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U12_GA(X1, maxcC_out_ga(X1, X2)) → U13_GA(X1, delcD_in_gga(X2, X1))
U13_GA(X1, delcD_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(t, .(t, X1))) → U12_GA(X1, maxcC_in_ga(X1))
MAXSORTA_IN_GA(.(t, .(f, X1))) → U18_GA(X1, maxcC_in_ga(X1))
U18_GA(X1, maxcC_out_ga(X1, X2)) → U19_GA(X1, delcE_in_gga(X2, X1))
U19_GA(X1, delcE_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(f, X1))) → U24_GA(X1, maxcF_in_ga(X1))
U24_GA(X1, maxcF_out_ga(X1, X2)) → U25_GA(X1, delcG_in_gga(X2, X1))
U25_GA(X1, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(t, X1))) → U30_GA(X1, maxcC_in_ga(X1))
U30_GA(X1, maxcC_out_ga(X1, X2)) → U31_GA(X1, delcH_in_gga(X2, X1))
U31_GA(X1, delcH_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)

The TRS R consists of the following rules:

delcH_in_gga(t, X1) → U57_gga(X1, delcJ_in_ga(.(t, X1)))
delcJ_in_ga(.(t, X1)) → delcJ_out_ga(.(t, X1), X1)
U57_gga(X1, delcJ_out_ga(.(t, X1), X2)) → delcH_out_gga(t, X1, .(f, X2))
maxcC_in_ga([]) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1)) → U48_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga(.(f, X1)) → U49_ga(X1, maxcC_in_ga(X1))
U49_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
delcG_in_gga(f, X1) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1) → U56_gga(X1, delcJ_in_ga(X1))
delcJ_in_ga([]) → delcJ_out_ga([], [])
delcJ_in_ga(.(f, X1)) → U53_ga(X1, delcJ_in_ga(X1))
U56_gga(X1, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
U53_ga(X1, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))
maxcF_in_ga([]) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1)) → U51_ga(X1, maxcF_in_ga(X1))
maxcF_in_ga(.(t, X1)) → U52_ga(X1, maxcC_in_ga(X1))
U52_ga(X1, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U51_ga(X1, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
delcE_in_gga(t, X1) → delcE_out_gga(t, X1, .(f, X1))
delcE_in_gga(f, X1) → U55_gga(X1, delcI_in_ga(.(f, X1)))
delcI_in_ga(.(f, X1)) → delcI_out_ga(.(f, X1), X1)
delcD_in_gga(t, X1) → delcD_out_gga(t, X1, .(t, X1))
delcD_in_gga(f, X1) → U54_gga(X1, delcI_in_ga(X1))
delcI_in_ga([]) → delcI_out_ga([], [])
delcI_in_ga(.(t, X1)) → U50_ga(X1, delcI_in_ga(X1))
U54_gga(X1, delcI_out_ga(X1, X2)) → delcD_out_gga(f, X1, .(t, .(t, X2)))
U50_ga(X1, delcI_out_ga(X1, X2)) → delcI_out_ga(.(t, X1), .(t, X2))

The set Q consists of the following terms:

maxcC_in_ga(x0)
delcD_in_gga(x0, x1)
delcE_in_gga(x0, x1)
maxcF_in_ga(x0)
delcG_in_gga(x0, x1)
delcH_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U54_gga(x0, x1)
U55_gga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
U57_gga(x0, x1)
delcI_in_ga(x0)
delcJ_in_ga(x0)
U50_ga(x0, x1)
U53_ga(x0, x1)

We have to consider all (P,Q,R)-chains.

(54) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


MAXSORTA_IN_GA(.(t, .(f, X1))) → U18_GA(X1, maxcC_in_ga(X1))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(.(x1, x2)) = x1   
POL(MAXSORTA_IN_GA(x1)) = x1   
POL(U12_GA(x1, x2)) = 1   
POL(U13_GA(x1, x2)) = x2   
POL(U18_GA(x1, x2)) = 0   
POL(U19_GA(x1, x2)) = x2   
POL(U24_GA(x1, x2)) = 0   
POL(U25_GA(x1, x2)) = x2   
POL(U30_GA(x1, x2)) = 0   
POL(U31_GA(x1, x2)) = x2   
POL(U48_ga(x1, x2)) = 0   
POL(U49_ga(x1, x2)) = 0   
POL(U50_ga(x1, x2)) = 0   
POL(U51_ga(x1, x2)) = 0   
POL(U52_ga(x1, x2)) = 0   
POL(U53_ga(x1, x2)) = 0   
POL(U54_gga(x1, x2)) = 1   
POL(U55_gga(x1, x2)) = 0   
POL(U56_gga(x1, x2)) = 0   
POL(U57_gga(x1, x2)) = 0   
POL([]) = 0   
POL(delcD_in_gga(x1, x2)) = 1   
POL(delcD_out_gga(x1, x2, x3)) = x3   
POL(delcE_in_gga(x1, x2)) = 0   
POL(delcE_out_gga(x1, x2, x3)) = x3   
POL(delcG_in_gga(x1, x2)) = 0   
POL(delcG_out_gga(x1, x2, x3)) = x3   
POL(delcH_in_gga(x1, x2)) = 0   
POL(delcH_out_gga(x1, x2, x3)) = x3   
POL(delcI_in_ga(x1)) = 0   
POL(delcI_out_ga(x1, x2)) = 0   
POL(delcJ_in_ga(x1)) = 0   
POL(delcJ_out_ga(x1, x2)) = 0   
POL(f) = 0   
POL(maxcC_in_ga(x1)) = 0   
POL(maxcC_out_ga(x1, x2)) = 0   
POL(maxcF_in_ga(x1)) = 0   
POL(maxcF_out_ga(x1, x2)) = 0   
POL(t) = 1   

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

delcD_in_gga(t, X1) → delcD_out_gga(t, X1, .(t, X1))
delcD_in_gga(f, X1) → U54_gga(X1, delcI_in_ga(X1))
delcE_in_gga(t, X1) → delcE_out_gga(t, X1, .(f, X1))
delcE_in_gga(f, X1) → U55_gga(X1, delcI_in_ga(.(f, X1)))
delcG_in_gga(f, X1) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1) → U56_gga(X1, delcJ_in_ga(X1))
delcH_in_gga(t, X1) → U57_gga(X1, delcJ_in_ga(.(t, X1)))
U57_gga(X1, delcJ_out_ga(.(t, X1), X2)) → delcH_out_gga(t, X1, .(f, X2))
U56_gga(X1, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
U54_gga(X1, delcI_out_ga(X1, X2)) → delcD_out_gga(f, X1, .(t, .(t, X2)))

(55) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U12_GA(X1, maxcC_out_ga(X1, X2)) → U13_GA(X1, delcD_in_gga(X2, X1))
U13_GA(X1, delcD_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(t, .(t, X1))) → U12_GA(X1, maxcC_in_ga(X1))
U18_GA(X1, maxcC_out_ga(X1, X2)) → U19_GA(X1, delcE_in_gga(X2, X1))
U19_GA(X1, delcE_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(f, X1))) → U24_GA(X1, maxcF_in_ga(X1))
U24_GA(X1, maxcF_out_ga(X1, X2)) → U25_GA(X1, delcG_in_gga(X2, X1))
U25_GA(X1, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(t, X1))) → U30_GA(X1, maxcC_in_ga(X1))
U30_GA(X1, maxcC_out_ga(X1, X2)) → U31_GA(X1, delcH_in_gga(X2, X1))
U31_GA(X1, delcH_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)

The TRS R consists of the following rules:

delcH_in_gga(t, X1) → U57_gga(X1, delcJ_in_ga(.(t, X1)))
delcJ_in_ga(.(t, X1)) → delcJ_out_ga(.(t, X1), X1)
U57_gga(X1, delcJ_out_ga(.(t, X1), X2)) → delcH_out_gga(t, X1, .(f, X2))
maxcC_in_ga([]) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1)) → U48_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga(.(f, X1)) → U49_ga(X1, maxcC_in_ga(X1))
U49_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
delcG_in_gga(f, X1) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1) → U56_gga(X1, delcJ_in_ga(X1))
delcJ_in_ga([]) → delcJ_out_ga([], [])
delcJ_in_ga(.(f, X1)) → U53_ga(X1, delcJ_in_ga(X1))
U56_gga(X1, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
U53_ga(X1, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))
maxcF_in_ga([]) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1)) → U51_ga(X1, maxcF_in_ga(X1))
maxcF_in_ga(.(t, X1)) → U52_ga(X1, maxcC_in_ga(X1))
U52_ga(X1, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U51_ga(X1, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
delcE_in_gga(t, X1) → delcE_out_gga(t, X1, .(f, X1))
delcE_in_gga(f, X1) → U55_gga(X1, delcI_in_ga(.(f, X1)))
delcI_in_ga(.(f, X1)) → delcI_out_ga(.(f, X1), X1)
delcD_in_gga(t, X1) → delcD_out_gga(t, X1, .(t, X1))
delcD_in_gga(f, X1) → U54_gga(X1, delcI_in_ga(X1))
delcI_in_ga([]) → delcI_out_ga([], [])
delcI_in_ga(.(t, X1)) → U50_ga(X1, delcI_in_ga(X1))
U54_gga(X1, delcI_out_ga(X1, X2)) → delcD_out_gga(f, X1, .(t, .(t, X2)))
U50_ga(X1, delcI_out_ga(X1, X2)) → delcI_out_ga(.(t, X1), .(t, X2))

The set Q consists of the following terms:

maxcC_in_ga(x0)
delcD_in_gga(x0, x1)
delcE_in_gga(x0, x1)
maxcF_in_ga(x0)
delcG_in_gga(x0, x1)
delcH_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U54_gga(x0, x1)
U55_gga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
U57_gga(x0, x1)
delcI_in_ga(x0)
delcJ_in_ga(x0)
U50_ga(x0, x1)
U53_ga(x0, x1)

We have to consider all (P,Q,R)-chains.

(56) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 2 less nodes.

(57) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U13_GA(X1, delcD_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(t, .(t, X1))) → U12_GA(X1, maxcC_in_ga(X1))
U12_GA(X1, maxcC_out_ga(X1, X2)) → U13_GA(X1, delcD_in_gga(X2, X1))
MAXSORTA_IN_GA(.(f, .(f, X1))) → U24_GA(X1, maxcF_in_ga(X1))
U24_GA(X1, maxcF_out_ga(X1, X2)) → U25_GA(X1, delcG_in_gga(X2, X1))
U25_GA(X1, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(t, X1))) → U30_GA(X1, maxcC_in_ga(X1))
U30_GA(X1, maxcC_out_ga(X1, X2)) → U31_GA(X1, delcH_in_gga(X2, X1))
U31_GA(X1, delcH_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)

The TRS R consists of the following rules:

delcH_in_gga(t, X1) → U57_gga(X1, delcJ_in_ga(.(t, X1)))
delcJ_in_ga(.(t, X1)) → delcJ_out_ga(.(t, X1), X1)
U57_gga(X1, delcJ_out_ga(.(t, X1), X2)) → delcH_out_gga(t, X1, .(f, X2))
maxcC_in_ga([]) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1)) → U48_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga(.(f, X1)) → U49_ga(X1, maxcC_in_ga(X1))
U49_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
delcG_in_gga(f, X1) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1) → U56_gga(X1, delcJ_in_ga(X1))
delcJ_in_ga([]) → delcJ_out_ga([], [])
delcJ_in_ga(.(f, X1)) → U53_ga(X1, delcJ_in_ga(X1))
U56_gga(X1, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
U53_ga(X1, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))
maxcF_in_ga([]) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1)) → U51_ga(X1, maxcF_in_ga(X1))
maxcF_in_ga(.(t, X1)) → U52_ga(X1, maxcC_in_ga(X1))
U52_ga(X1, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U51_ga(X1, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
delcE_in_gga(t, X1) → delcE_out_gga(t, X1, .(f, X1))
delcE_in_gga(f, X1) → U55_gga(X1, delcI_in_ga(.(f, X1)))
delcI_in_ga(.(f, X1)) → delcI_out_ga(.(f, X1), X1)
delcD_in_gga(t, X1) → delcD_out_gga(t, X1, .(t, X1))
delcD_in_gga(f, X1) → U54_gga(X1, delcI_in_ga(X1))
delcI_in_ga([]) → delcI_out_ga([], [])
delcI_in_ga(.(t, X1)) → U50_ga(X1, delcI_in_ga(X1))
U54_gga(X1, delcI_out_ga(X1, X2)) → delcD_out_gga(f, X1, .(t, .(t, X2)))
U50_ga(X1, delcI_out_ga(X1, X2)) → delcI_out_ga(.(t, X1), .(t, X2))

The set Q consists of the following terms:

maxcC_in_ga(x0)
delcD_in_gga(x0, x1)
delcE_in_gga(x0, x1)
maxcF_in_ga(x0)
delcG_in_gga(x0, x1)
delcH_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U54_gga(x0, x1)
U55_gga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
U57_gga(x0, x1)
delcI_in_ga(x0)
delcJ_in_ga(x0)
U50_ga(x0, x1)
U53_ga(x0, x1)

We have to consider all (P,Q,R)-chains.

(58) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(59) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U13_GA(X1, delcD_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(t, .(t, X1))) → U12_GA(X1, maxcC_in_ga(X1))
U12_GA(X1, maxcC_out_ga(X1, X2)) → U13_GA(X1, delcD_in_gga(X2, X1))
MAXSORTA_IN_GA(.(f, .(f, X1))) → U24_GA(X1, maxcF_in_ga(X1))
U24_GA(X1, maxcF_out_ga(X1, X2)) → U25_GA(X1, delcG_in_gga(X2, X1))
U25_GA(X1, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(t, X1))) → U30_GA(X1, maxcC_in_ga(X1))
U30_GA(X1, maxcC_out_ga(X1, X2)) → U31_GA(X1, delcH_in_gga(X2, X1))
U31_GA(X1, delcH_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)

The TRS R consists of the following rules:

delcH_in_gga(t, X1) → U57_gga(X1, delcJ_in_ga(.(t, X1)))
delcJ_in_ga(.(t, X1)) → delcJ_out_ga(.(t, X1), X1)
U57_gga(X1, delcJ_out_ga(.(t, X1), X2)) → delcH_out_gga(t, X1, .(f, X2))
maxcC_in_ga([]) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1)) → U48_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga(.(f, X1)) → U49_ga(X1, maxcC_in_ga(X1))
U49_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
delcG_in_gga(f, X1) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1) → U56_gga(X1, delcJ_in_ga(X1))
delcJ_in_ga([]) → delcJ_out_ga([], [])
delcJ_in_ga(.(f, X1)) → U53_ga(X1, delcJ_in_ga(X1))
U56_gga(X1, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
U53_ga(X1, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))
maxcF_in_ga([]) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1)) → U51_ga(X1, maxcF_in_ga(X1))
maxcF_in_ga(.(t, X1)) → U52_ga(X1, maxcC_in_ga(X1))
U52_ga(X1, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U51_ga(X1, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
delcD_in_gga(t, X1) → delcD_out_gga(t, X1, .(t, X1))
delcD_in_gga(f, X1) → U54_gga(X1, delcI_in_ga(X1))
delcI_in_ga(.(f, X1)) → delcI_out_ga(.(f, X1), X1)
delcI_in_ga([]) → delcI_out_ga([], [])
delcI_in_ga(.(t, X1)) → U50_ga(X1, delcI_in_ga(X1))
U54_gga(X1, delcI_out_ga(X1, X2)) → delcD_out_gga(f, X1, .(t, .(t, X2)))
U50_ga(X1, delcI_out_ga(X1, X2)) → delcI_out_ga(.(t, X1), .(t, X2))

The set Q consists of the following terms:

maxcC_in_ga(x0)
delcD_in_gga(x0, x1)
delcE_in_gga(x0, x1)
maxcF_in_ga(x0)
delcG_in_gga(x0, x1)
delcH_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U54_gga(x0, x1)
U55_gga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
U57_gga(x0, x1)
delcI_in_ga(x0)
delcJ_in_ga(x0)
U50_ga(x0, x1)
U53_ga(x0, x1)

We have to consider all (P,Q,R)-chains.

(60) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

delcE_in_gga(x0, x1)
U55_gga(x0, x1)

(61) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U13_GA(X1, delcD_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(t, .(t, X1))) → U12_GA(X1, maxcC_in_ga(X1))
U12_GA(X1, maxcC_out_ga(X1, X2)) → U13_GA(X1, delcD_in_gga(X2, X1))
MAXSORTA_IN_GA(.(f, .(f, X1))) → U24_GA(X1, maxcF_in_ga(X1))
U24_GA(X1, maxcF_out_ga(X1, X2)) → U25_GA(X1, delcG_in_gga(X2, X1))
U25_GA(X1, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(t, X1))) → U30_GA(X1, maxcC_in_ga(X1))
U30_GA(X1, maxcC_out_ga(X1, X2)) → U31_GA(X1, delcH_in_gga(X2, X1))
U31_GA(X1, delcH_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)

The TRS R consists of the following rules:

delcH_in_gga(t, X1) → U57_gga(X1, delcJ_in_ga(.(t, X1)))
delcJ_in_ga(.(t, X1)) → delcJ_out_ga(.(t, X1), X1)
U57_gga(X1, delcJ_out_ga(.(t, X1), X2)) → delcH_out_gga(t, X1, .(f, X2))
maxcC_in_ga([]) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1)) → U48_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga(.(f, X1)) → U49_ga(X1, maxcC_in_ga(X1))
U49_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
delcG_in_gga(f, X1) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1) → U56_gga(X1, delcJ_in_ga(X1))
delcJ_in_ga([]) → delcJ_out_ga([], [])
delcJ_in_ga(.(f, X1)) → U53_ga(X1, delcJ_in_ga(X1))
U56_gga(X1, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
U53_ga(X1, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))
maxcF_in_ga([]) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1)) → U51_ga(X1, maxcF_in_ga(X1))
maxcF_in_ga(.(t, X1)) → U52_ga(X1, maxcC_in_ga(X1))
U52_ga(X1, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U51_ga(X1, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
delcD_in_gga(t, X1) → delcD_out_gga(t, X1, .(t, X1))
delcD_in_gga(f, X1) → U54_gga(X1, delcI_in_ga(X1))
delcI_in_ga(.(f, X1)) → delcI_out_ga(.(f, X1), X1)
delcI_in_ga([]) → delcI_out_ga([], [])
delcI_in_ga(.(t, X1)) → U50_ga(X1, delcI_in_ga(X1))
U54_gga(X1, delcI_out_ga(X1, X2)) → delcD_out_gga(f, X1, .(t, .(t, X2)))
U50_ga(X1, delcI_out_ga(X1, X2)) → delcI_out_ga(.(t, X1), .(t, X2))

The set Q consists of the following terms:

maxcC_in_ga(x0)
delcD_in_gga(x0, x1)
maxcF_in_ga(x0)
delcG_in_gga(x0, x1)
delcH_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U54_gga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
U57_gga(x0, x1)
delcI_in_ga(x0)
delcJ_in_ga(x0)
U50_ga(x0, x1)
U53_ga(x0, x1)

We have to consider all (P,Q,R)-chains.

(62) QDPQMonotonicMRRProof (EQUIVALENT transformation)

By using the Q-monotonic rule removal processor with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented such that it always occurs at a strongly monotonic position in a (P,Q,R)-chain.

Strictly oriented rules of the TRS R:

U54_gga(X1, delcI_out_ga(X1, X2)) → delcD_out_gga(f, X1, .(t, .(t, X2)))

Used ordering: Polynomial interpretation [POLO]:

POL(.(x1, x2)) = 0   
POL(MAXSORTA_IN_GA(x1)) = 0   
POL(U12_GA(x1, x2)) = 2·x2   
POL(U13_GA(x1, x2)) = x2   
POL(U24_GA(x1, x2)) = 0   
POL(U25_GA(x1, x2)) = 0   
POL(U30_GA(x1, x2)) = 0   
POL(U31_GA(x1, x2)) = 0   
POL(U48_ga(x1, x2)) = 2·x2   
POL(U49_ga(x1, x2)) = x2   
POL(U50_ga(x1, x2)) = 0   
POL(U51_ga(x1, x2)) = 0   
POL(U52_ga(x1, x2)) = 0   
POL(U53_ga(x1, x2)) = 1   
POL(U54_gga(x1, x2)) = 2   
POL(U56_gga(x1, x2)) = 2·x1   
POL(U57_gga(x1, x2)) = 0   
POL([]) = 0   
POL(delcD_in_gga(x1, x2)) = x1   
POL(delcD_out_gga(x1, x2, x3)) = 0   
POL(delcG_in_gga(x1, x2)) = 2·x2   
POL(delcG_out_gga(x1, x2, x3)) = x2   
POL(delcH_in_gga(x1, x2)) = 1   
POL(delcH_out_gga(x1, x2, x3)) = x1   
POL(delcI_in_ga(x1)) = 0   
POL(delcI_out_ga(x1, x2)) = 2·x1   
POL(delcJ_in_ga(x1)) = 2   
POL(delcJ_out_ga(x1, x2)) = 1   
POL(f) = 2   
POL(maxcC_in_ga(x1)) = 0   
POL(maxcC_out_ga(x1, x2)) = 2·x2   
POL(maxcF_in_ga(x1)) = 0   
POL(maxcF_out_ga(x1, x2)) = 2·x1   
POL(t) = 0   

(63) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U13_GA(X1, delcD_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(t, .(t, X1))) → U12_GA(X1, maxcC_in_ga(X1))
U12_GA(X1, maxcC_out_ga(X1, X2)) → U13_GA(X1, delcD_in_gga(X2, X1))
MAXSORTA_IN_GA(.(f, .(f, X1))) → U24_GA(X1, maxcF_in_ga(X1))
U24_GA(X1, maxcF_out_ga(X1, X2)) → U25_GA(X1, delcG_in_gga(X2, X1))
U25_GA(X1, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(t, X1))) → U30_GA(X1, maxcC_in_ga(X1))
U30_GA(X1, maxcC_out_ga(X1, X2)) → U31_GA(X1, delcH_in_gga(X2, X1))
U31_GA(X1, delcH_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)

The TRS R consists of the following rules:

delcH_in_gga(t, X1) → U57_gga(X1, delcJ_in_ga(.(t, X1)))
delcJ_in_ga(.(t, X1)) → delcJ_out_ga(.(t, X1), X1)
U57_gga(X1, delcJ_out_ga(.(t, X1), X2)) → delcH_out_gga(t, X1, .(f, X2))
maxcC_in_ga([]) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1)) → U48_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga(.(f, X1)) → U49_ga(X1, maxcC_in_ga(X1))
U49_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
delcG_in_gga(f, X1) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1) → U56_gga(X1, delcJ_in_ga(X1))
delcJ_in_ga([]) → delcJ_out_ga([], [])
delcJ_in_ga(.(f, X1)) → U53_ga(X1, delcJ_in_ga(X1))
U56_gga(X1, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
U53_ga(X1, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))
maxcF_in_ga([]) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1)) → U51_ga(X1, maxcF_in_ga(X1))
maxcF_in_ga(.(t, X1)) → U52_ga(X1, maxcC_in_ga(X1))
U52_ga(X1, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U51_ga(X1, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
delcD_in_gga(t, X1) → delcD_out_gga(t, X1, .(t, X1))
delcD_in_gga(f, X1) → U54_gga(X1, delcI_in_ga(X1))
delcI_in_ga(.(f, X1)) → delcI_out_ga(.(f, X1), X1)
delcI_in_ga([]) → delcI_out_ga([], [])
delcI_in_ga(.(t, X1)) → U50_ga(X1, delcI_in_ga(X1))
U50_ga(X1, delcI_out_ga(X1, X2)) → delcI_out_ga(.(t, X1), .(t, X2))

The set Q consists of the following terms:

maxcC_in_ga(x0)
delcD_in_gga(x0, x1)
maxcF_in_ga(x0)
delcG_in_gga(x0, x1)
delcH_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U54_gga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
U57_gga(x0, x1)
delcI_in_ga(x0)
delcJ_in_ga(x0)
U50_ga(x0, x1)
U53_ga(x0, x1)

We have to consider all (P,Q,R)-chains.

(64) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


MAXSORTA_IN_GA(.(t, .(t, X1))) → U12_GA(X1, maxcC_in_ga(X1))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(.(x1, x2)) = x1 + x2   
POL(MAXSORTA_IN_GA(x1)) = x1   
POL(U12_GA(x1, x2)) = 1 + x1   
POL(U13_GA(x1, x2)) = x2   
POL(U24_GA(x1, x2)) = x1   
POL(U25_GA(x1, x2)) = x2   
POL(U30_GA(x1, x2)) = 1 + x1   
POL(U31_GA(x1, x2)) = x2   
POL(U48_ga(x1, x2)) = 0   
POL(U49_ga(x1, x2)) = 0   
POL(U50_ga(x1, x2)) = 0   
POL(U51_ga(x1, x2)) = 0   
POL(U52_ga(x1, x2)) = 0   
POL(U53_ga(x1, x2)) = x2   
POL(U54_gga(x1, x2)) = 0   
POL(U56_gga(x1, x2)) = x2   
POL(U57_gga(x1, x2)) = x2   
POL([]) = 0   
POL(delcD_in_gga(x1, x2)) = 1 + x2   
POL(delcD_out_gga(x1, x2, x3)) = x3   
POL(delcG_in_gga(x1, x2)) = x2   
POL(delcG_out_gga(x1, x2, x3)) = x3   
POL(delcH_in_gga(x1, x2)) = 1 + x2   
POL(delcH_out_gga(x1, x2, x3)) = x3   
POL(delcI_in_ga(x1)) = 0   
POL(delcI_out_ga(x1, x2)) = 0   
POL(delcJ_in_ga(x1)) = x1   
POL(delcJ_out_ga(x1, x2)) = x2   
POL(f) = 0   
POL(maxcC_in_ga(x1)) = 0   
POL(maxcC_out_ga(x1, x2)) = 0   
POL(maxcF_in_ga(x1)) = 0   
POL(maxcF_out_ga(x1, x2)) = 0   
POL(t) = 1   

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

delcD_in_gga(t, X1) → delcD_out_gga(t, X1, .(t, X1))
delcD_in_gga(f, X1) → U54_gga(X1, delcI_in_ga(X1))
delcG_in_gga(f, X1) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1) → U56_gga(X1, delcJ_in_ga(X1))
delcH_in_gga(t, X1) → U57_gga(X1, delcJ_in_ga(.(t, X1)))
delcJ_in_ga(.(t, X1)) → delcJ_out_ga(.(t, X1), X1)
U57_gga(X1, delcJ_out_ga(.(t, X1), X2)) → delcH_out_gga(t, X1, .(f, X2))
delcJ_in_ga([]) → delcJ_out_ga([], [])
delcJ_in_ga(.(f, X1)) → U53_ga(X1, delcJ_in_ga(X1))
U56_gga(X1, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
U53_ga(X1, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))

(65) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U13_GA(X1, delcD_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
U12_GA(X1, maxcC_out_ga(X1, X2)) → U13_GA(X1, delcD_in_gga(X2, X1))
MAXSORTA_IN_GA(.(f, .(f, X1))) → U24_GA(X1, maxcF_in_ga(X1))
U24_GA(X1, maxcF_out_ga(X1, X2)) → U25_GA(X1, delcG_in_gga(X2, X1))
U25_GA(X1, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(t, X1))) → U30_GA(X1, maxcC_in_ga(X1))
U30_GA(X1, maxcC_out_ga(X1, X2)) → U31_GA(X1, delcH_in_gga(X2, X1))
U31_GA(X1, delcH_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)

The TRS R consists of the following rules:

delcH_in_gga(t, X1) → U57_gga(X1, delcJ_in_ga(.(t, X1)))
delcJ_in_ga(.(t, X1)) → delcJ_out_ga(.(t, X1), X1)
U57_gga(X1, delcJ_out_ga(.(t, X1), X2)) → delcH_out_gga(t, X1, .(f, X2))
maxcC_in_ga([]) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1)) → U48_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga(.(f, X1)) → U49_ga(X1, maxcC_in_ga(X1))
U49_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
delcG_in_gga(f, X1) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1) → U56_gga(X1, delcJ_in_ga(X1))
delcJ_in_ga([]) → delcJ_out_ga([], [])
delcJ_in_ga(.(f, X1)) → U53_ga(X1, delcJ_in_ga(X1))
U56_gga(X1, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
U53_ga(X1, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))
maxcF_in_ga([]) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1)) → U51_ga(X1, maxcF_in_ga(X1))
maxcF_in_ga(.(t, X1)) → U52_ga(X1, maxcC_in_ga(X1))
U52_ga(X1, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U51_ga(X1, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
delcD_in_gga(t, X1) → delcD_out_gga(t, X1, .(t, X1))
delcD_in_gga(f, X1) → U54_gga(X1, delcI_in_ga(X1))
delcI_in_ga(.(f, X1)) → delcI_out_ga(.(f, X1), X1)
delcI_in_ga([]) → delcI_out_ga([], [])
delcI_in_ga(.(t, X1)) → U50_ga(X1, delcI_in_ga(X1))
U50_ga(X1, delcI_out_ga(X1, X2)) → delcI_out_ga(.(t, X1), .(t, X2))

The set Q consists of the following terms:

maxcC_in_ga(x0)
delcD_in_gga(x0, x1)
maxcF_in_ga(x0)
delcG_in_gga(x0, x1)
delcH_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U54_gga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
U57_gga(x0, x1)
delcI_in_ga(x0)
delcJ_in_ga(x0)
U50_ga(x0, x1)
U53_ga(x0, x1)

We have to consider all (P,Q,R)-chains.

(66) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 2 less nodes.

(67) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U24_GA(X1, maxcF_out_ga(X1, X2)) → U25_GA(X1, delcG_in_gga(X2, X1))
U25_GA(X1, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(f, X1))) → U24_GA(X1, maxcF_in_ga(X1))
MAXSORTA_IN_GA(.(f, .(t, X1))) → U30_GA(X1, maxcC_in_ga(X1))
U30_GA(X1, maxcC_out_ga(X1, X2)) → U31_GA(X1, delcH_in_gga(X2, X1))
U31_GA(X1, delcH_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)

The TRS R consists of the following rules:

delcH_in_gga(t, X1) → U57_gga(X1, delcJ_in_ga(.(t, X1)))
delcJ_in_ga(.(t, X1)) → delcJ_out_ga(.(t, X1), X1)
U57_gga(X1, delcJ_out_ga(.(t, X1), X2)) → delcH_out_gga(t, X1, .(f, X2))
maxcC_in_ga([]) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1)) → U48_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga(.(f, X1)) → U49_ga(X1, maxcC_in_ga(X1))
U49_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
delcG_in_gga(f, X1) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1) → U56_gga(X1, delcJ_in_ga(X1))
delcJ_in_ga([]) → delcJ_out_ga([], [])
delcJ_in_ga(.(f, X1)) → U53_ga(X1, delcJ_in_ga(X1))
U56_gga(X1, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
U53_ga(X1, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))
maxcF_in_ga([]) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1)) → U51_ga(X1, maxcF_in_ga(X1))
maxcF_in_ga(.(t, X1)) → U52_ga(X1, maxcC_in_ga(X1))
U52_ga(X1, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U51_ga(X1, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
delcD_in_gga(t, X1) → delcD_out_gga(t, X1, .(t, X1))
delcD_in_gga(f, X1) → U54_gga(X1, delcI_in_ga(X1))
delcI_in_ga(.(f, X1)) → delcI_out_ga(.(f, X1), X1)
delcI_in_ga([]) → delcI_out_ga([], [])
delcI_in_ga(.(t, X1)) → U50_ga(X1, delcI_in_ga(X1))
U50_ga(X1, delcI_out_ga(X1, X2)) → delcI_out_ga(.(t, X1), .(t, X2))

The set Q consists of the following terms:

maxcC_in_ga(x0)
delcD_in_gga(x0, x1)
maxcF_in_ga(x0)
delcG_in_gga(x0, x1)
delcH_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U54_gga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
U57_gga(x0, x1)
delcI_in_ga(x0)
delcJ_in_ga(x0)
U50_ga(x0, x1)
U53_ga(x0, x1)

We have to consider all (P,Q,R)-chains.

(68) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(69) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U24_GA(X1, maxcF_out_ga(X1, X2)) → U25_GA(X1, delcG_in_gga(X2, X1))
U25_GA(X1, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(f, X1))) → U24_GA(X1, maxcF_in_ga(X1))
MAXSORTA_IN_GA(.(f, .(t, X1))) → U30_GA(X1, maxcC_in_ga(X1))
U30_GA(X1, maxcC_out_ga(X1, X2)) → U31_GA(X1, delcH_in_gga(X2, X1))
U31_GA(X1, delcH_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)

The TRS R consists of the following rules:

delcH_in_gga(t, X1) → U57_gga(X1, delcJ_in_ga(.(t, X1)))
delcJ_in_ga(.(t, X1)) → delcJ_out_ga(.(t, X1), X1)
U57_gga(X1, delcJ_out_ga(.(t, X1), X2)) → delcH_out_gga(t, X1, .(f, X2))
maxcC_in_ga([]) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1)) → U48_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga(.(f, X1)) → U49_ga(X1, maxcC_in_ga(X1))
U49_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
maxcF_in_ga([]) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1)) → U51_ga(X1, maxcF_in_ga(X1))
maxcF_in_ga(.(t, X1)) → U52_ga(X1, maxcC_in_ga(X1))
U52_ga(X1, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U51_ga(X1, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
delcG_in_gga(f, X1) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1) → U56_gga(X1, delcJ_in_ga(X1))
delcJ_in_ga([]) → delcJ_out_ga([], [])
delcJ_in_ga(.(f, X1)) → U53_ga(X1, delcJ_in_ga(X1))
U56_gga(X1, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
U53_ga(X1, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))

The set Q consists of the following terms:

maxcC_in_ga(x0)
delcD_in_gga(x0, x1)
maxcF_in_ga(x0)
delcG_in_gga(x0, x1)
delcH_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U54_gga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
U57_gga(x0, x1)
delcI_in_ga(x0)
delcJ_in_ga(x0)
U50_ga(x0, x1)
U53_ga(x0, x1)

We have to consider all (P,Q,R)-chains.

(70) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

delcD_in_gga(x0, x1)
U54_gga(x0, x1)
delcI_in_ga(x0)
U50_ga(x0, x1)

(71) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U24_GA(X1, maxcF_out_ga(X1, X2)) → U25_GA(X1, delcG_in_gga(X2, X1))
U25_GA(X1, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(f, X1))) → U24_GA(X1, maxcF_in_ga(X1))
MAXSORTA_IN_GA(.(f, .(t, X1))) → U30_GA(X1, maxcC_in_ga(X1))
U30_GA(X1, maxcC_out_ga(X1, X2)) → U31_GA(X1, delcH_in_gga(X2, X1))
U31_GA(X1, delcH_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)

The TRS R consists of the following rules:

delcH_in_gga(t, X1) → U57_gga(X1, delcJ_in_ga(.(t, X1)))
delcJ_in_ga(.(t, X1)) → delcJ_out_ga(.(t, X1), X1)
U57_gga(X1, delcJ_out_ga(.(t, X1), X2)) → delcH_out_gga(t, X1, .(f, X2))
maxcC_in_ga([]) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1)) → U48_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga(.(f, X1)) → U49_ga(X1, maxcC_in_ga(X1))
U49_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
maxcF_in_ga([]) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1)) → U51_ga(X1, maxcF_in_ga(X1))
maxcF_in_ga(.(t, X1)) → U52_ga(X1, maxcC_in_ga(X1))
U52_ga(X1, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U51_ga(X1, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
delcG_in_gga(f, X1) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1) → U56_gga(X1, delcJ_in_ga(X1))
delcJ_in_ga([]) → delcJ_out_ga([], [])
delcJ_in_ga(.(f, X1)) → U53_ga(X1, delcJ_in_ga(X1))
U56_gga(X1, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
U53_ga(X1, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))

The set Q consists of the following terms:

maxcC_in_ga(x0)
maxcF_in_ga(x0)
delcG_in_gga(x0, x1)
delcH_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
U57_gga(x0, x1)
delcJ_in_ga(x0)
U53_ga(x0, x1)

We have to consider all (P,Q,R)-chains.

(72) QDPQMonotonicMRRProof (EQUIVALENT transformation)

By using the Q-monotonic rule removal processor with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented such that it always occurs at a strongly monotonic position in a (P,Q,R)-chain.

Strictly oriented rules of the TRS R:

delcJ_in_ga(.(t, X1)) → delcJ_out_ga(.(t, X1), X1)

Used ordering: Polynomial interpretation [POLO]:

POL(.(x1, x2)) = 2·x1 + x2   
POL(MAXSORTA_IN_GA(x1)) = x1   
POL(U24_GA(x1, x2)) = x1   
POL(U25_GA(x1, x2)) = x2   
POL(U30_GA(x1, x2)) = x1 + 2·x2   
POL(U31_GA(x1, x2)) = x2   
POL(U48_ga(x1, x2)) = x2   
POL(U49_ga(x1, x2)) = x2   
POL(U51_ga(x1, x2)) = 0   
POL(U52_ga(x1, x2)) = 0   
POL(U53_ga(x1, x2)) = x2   
POL(U56_gga(x1, x2)) = x2   
POL(U57_gga(x1, x2)) = x2   
POL([]) = 0   
POL(delcG_in_gga(x1, x2)) = x2   
POL(delcG_out_gga(x1, x2, x3)) = x3   
POL(delcH_in_gga(x1, x2)) = 2·x1 + x2   
POL(delcH_out_gga(x1, x2, x3)) = x3   
POL(delcJ_in_ga(x1)) = x1   
POL(delcJ_out_ga(x1, x2)) = x2   
POL(f) = 0   
POL(maxcC_in_ga(x1)) = 2   
POL(maxcC_out_ga(x1, x2)) = x2   
POL(maxcF_in_ga(x1)) = 1   
POL(maxcF_out_ga(x1, x2)) = 0   
POL(t) = 2   

(73) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U24_GA(X1, maxcF_out_ga(X1, X2)) → U25_GA(X1, delcG_in_gga(X2, X1))
U25_GA(X1, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(f, X1))) → U24_GA(X1, maxcF_in_ga(X1))
MAXSORTA_IN_GA(.(f, .(t, X1))) → U30_GA(X1, maxcC_in_ga(X1))
U30_GA(X1, maxcC_out_ga(X1, X2)) → U31_GA(X1, delcH_in_gga(X2, X1))
U31_GA(X1, delcH_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)

The TRS R consists of the following rules:

delcH_in_gga(t, X1) → U57_gga(X1, delcJ_in_ga(.(t, X1)))
U57_gga(X1, delcJ_out_ga(.(t, X1), X2)) → delcH_out_gga(t, X1, .(f, X2))
maxcC_in_ga([]) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1)) → U48_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga(.(f, X1)) → U49_ga(X1, maxcC_in_ga(X1))
U49_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
maxcF_in_ga([]) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1)) → U51_ga(X1, maxcF_in_ga(X1))
maxcF_in_ga(.(t, X1)) → U52_ga(X1, maxcC_in_ga(X1))
U52_ga(X1, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U51_ga(X1, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
delcG_in_gga(f, X1) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1) → U56_gga(X1, delcJ_in_ga(X1))
delcJ_in_ga([]) → delcJ_out_ga([], [])
delcJ_in_ga(.(f, X1)) → U53_ga(X1, delcJ_in_ga(X1))
U56_gga(X1, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
U53_ga(X1, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))

The set Q consists of the following terms:

maxcC_in_ga(x0)
maxcF_in_ga(x0)
delcG_in_gga(x0, x1)
delcH_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
U57_gga(x0, x1)
delcJ_in_ga(x0)
U53_ga(x0, x1)

We have to consider all (P,Q,R)-chains.

(74) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 3 less nodes.

(75) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U25_GA(X1, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(f, X1))) → U24_GA(X1, maxcF_in_ga(X1))
U24_GA(X1, maxcF_out_ga(X1, X2)) → U25_GA(X1, delcG_in_gga(X2, X1))

The TRS R consists of the following rules:

delcH_in_gga(t, X1) → U57_gga(X1, delcJ_in_ga(.(t, X1)))
U57_gga(X1, delcJ_out_ga(.(t, X1), X2)) → delcH_out_gga(t, X1, .(f, X2))
maxcC_in_ga([]) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1)) → U48_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga(.(f, X1)) → U49_ga(X1, maxcC_in_ga(X1))
U49_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
maxcF_in_ga([]) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1)) → U51_ga(X1, maxcF_in_ga(X1))
maxcF_in_ga(.(t, X1)) → U52_ga(X1, maxcC_in_ga(X1))
U52_ga(X1, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U51_ga(X1, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
delcG_in_gga(f, X1) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1) → U56_gga(X1, delcJ_in_ga(X1))
delcJ_in_ga([]) → delcJ_out_ga([], [])
delcJ_in_ga(.(f, X1)) → U53_ga(X1, delcJ_in_ga(X1))
U56_gga(X1, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
U53_ga(X1, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))

The set Q consists of the following terms:

maxcC_in_ga(x0)
maxcF_in_ga(x0)
delcG_in_gga(x0, x1)
delcH_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
U57_gga(x0, x1)
delcJ_in_ga(x0)
U53_ga(x0, x1)

We have to consider all (P,Q,R)-chains.

(76) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(77) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U25_GA(X1, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(f, X1))) → U24_GA(X1, maxcF_in_ga(X1))
U24_GA(X1, maxcF_out_ga(X1, X2)) → U25_GA(X1, delcG_in_gga(X2, X1))

The TRS R consists of the following rules:

delcG_in_gga(f, X1) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1) → U56_gga(X1, delcJ_in_ga(X1))
delcJ_in_ga([]) → delcJ_out_ga([], [])
delcJ_in_ga(.(f, X1)) → U53_ga(X1, delcJ_in_ga(X1))
U56_gga(X1, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
U53_ga(X1, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))
maxcF_in_ga([]) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1)) → U51_ga(X1, maxcF_in_ga(X1))
maxcF_in_ga(.(t, X1)) → U52_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga([]) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1)) → U48_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga(.(f, X1)) → U49_ga(X1, maxcC_in_ga(X1))
U52_ga(X1, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U49_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
U51_ga(X1, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)

The set Q consists of the following terms:

maxcC_in_ga(x0)
maxcF_in_ga(x0)
delcG_in_gga(x0, x1)
delcH_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
U57_gga(x0, x1)
delcJ_in_ga(x0)
U53_ga(x0, x1)

We have to consider all (P,Q,R)-chains.

(78) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

delcH_in_gga(x0, x1)
U57_gga(x0, x1)

(79) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U25_GA(X1, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(f, X1))) → U24_GA(X1, maxcF_in_ga(X1))
U24_GA(X1, maxcF_out_ga(X1, X2)) → U25_GA(X1, delcG_in_gga(X2, X1))

The TRS R consists of the following rules:

delcG_in_gga(f, X1) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1) → U56_gga(X1, delcJ_in_ga(X1))
delcJ_in_ga([]) → delcJ_out_ga([], [])
delcJ_in_ga(.(f, X1)) → U53_ga(X1, delcJ_in_ga(X1))
U56_gga(X1, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
U53_ga(X1, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))
maxcF_in_ga([]) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1)) → U51_ga(X1, maxcF_in_ga(X1))
maxcF_in_ga(.(t, X1)) → U52_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga([]) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1)) → U48_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga(.(f, X1)) → U49_ga(X1, maxcC_in_ga(X1))
U52_ga(X1, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U49_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
U51_ga(X1, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)

The set Q consists of the following terms:

maxcC_in_ga(x0)
maxcF_in_ga(x0)
delcG_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
delcJ_in_ga(x0)
U53_ga(x0, x1)

We have to consider all (P,Q,R)-chains.

(80) QDPQMonotonicMRRProof (EQUIVALENT transformation)

By using the Q-monotonic rule removal processor with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented such that it always occurs at a strongly monotonic position in a (P,Q,R)-chain.

Strictly oriented rules of the TRS R:

delcG_in_gga(t, X1) → U56_gga(X1, delcJ_in_ga(X1))

Used ordering: Polynomial interpretation [POLO]:

POL(.(x1, x2)) = 2·x1 + 2·x2   
POL(MAXSORTA_IN_GA(x1)) = x1   
POL(U24_GA(x1, x2)) = 2·x1 + x2   
POL(U25_GA(x1, x2)) = x2   
POL(U48_ga(x1, x2)) = x2   
POL(U49_ga(x1, x2)) = x2   
POL(U51_ga(x1, x2)) = 2·x2   
POL(U52_ga(x1, x2)) = 2·x2   
POL(U53_ga(x1, x2)) = 2·x2   
POL(U56_gga(x1, x2)) = 2·x2   
POL([]) = 0   
POL(delcG_in_gga(x1, x2)) = 2·x1 + 2·x2   
POL(delcG_out_gga(x1, x2, x3)) = x3   
POL(delcJ_in_ga(x1)) = 0   
POL(delcJ_out_ga(x1, x2)) = 2·x2   
POL(f) = 0   
POL(maxcC_in_ga(x1)) = 2   
POL(maxcC_out_ga(x1, x2)) = x2   
POL(maxcF_in_ga(x1)) = x1   
POL(maxcF_out_ga(x1, x2)) = 2·x2   
POL(t) = 2   

(81) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U25_GA(X1, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(f, X1))) → U24_GA(X1, maxcF_in_ga(X1))
U24_GA(X1, maxcF_out_ga(X1, X2)) → U25_GA(X1, delcG_in_gga(X2, X1))

The TRS R consists of the following rules:

delcG_in_gga(f, X1) → delcG_out_gga(f, X1, .(f, X1))
delcJ_in_ga([]) → delcJ_out_ga([], [])
delcJ_in_ga(.(f, X1)) → U53_ga(X1, delcJ_in_ga(X1))
U56_gga(X1, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
U53_ga(X1, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))
maxcF_in_ga([]) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1)) → U51_ga(X1, maxcF_in_ga(X1))
maxcF_in_ga(.(t, X1)) → U52_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga([]) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1)) → U48_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga(.(f, X1)) → U49_ga(X1, maxcC_in_ga(X1))
U52_ga(X1, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U49_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
U51_ga(X1, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)

The set Q consists of the following terms:

maxcC_in_ga(x0)
maxcF_in_ga(x0)
delcG_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
delcJ_in_ga(x0)
U53_ga(x0, x1)

We have to consider all (P,Q,R)-chains.

(82) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(83) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U25_GA(X1, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(f, X1))) → U24_GA(X1, maxcF_in_ga(X1))
U24_GA(X1, maxcF_out_ga(X1, X2)) → U25_GA(X1, delcG_in_gga(X2, X1))

The TRS R consists of the following rules:

delcG_in_gga(f, X1) → delcG_out_gga(f, X1, .(f, X1))
maxcF_in_ga([]) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1)) → U51_ga(X1, maxcF_in_ga(X1))
maxcF_in_ga(.(t, X1)) → U52_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga([]) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1)) → U48_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga(.(f, X1)) → U49_ga(X1, maxcC_in_ga(X1))
U52_ga(X1, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U49_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
U51_ga(X1, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)

The set Q consists of the following terms:

maxcC_in_ga(x0)
maxcF_in_ga(x0)
delcG_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
delcJ_in_ga(x0)
U53_ga(x0, x1)

We have to consider all (P,Q,R)-chains.

(84) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

U56_gga(x0, x1)
delcJ_in_ga(x0)
U53_ga(x0, x1)

(85) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U25_GA(X1, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(f, X1))) → U24_GA(X1, maxcF_in_ga(X1))
U24_GA(X1, maxcF_out_ga(X1, X2)) → U25_GA(X1, delcG_in_gga(X2, X1))

The TRS R consists of the following rules:

delcG_in_gga(f, X1) → delcG_out_gga(f, X1, .(f, X1))
maxcF_in_ga([]) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1)) → U51_ga(X1, maxcF_in_ga(X1))
maxcF_in_ga(.(t, X1)) → U52_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga([]) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1)) → U48_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga(.(f, X1)) → U49_ga(X1, maxcC_in_ga(X1))
U52_ga(X1, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U49_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
U51_ga(X1, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)

The set Q consists of the following terms:

maxcC_in_ga(x0)
maxcF_in_ga(x0)
delcG_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)

We have to consider all (P,Q,R)-chains.

(86) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule U24_GA(X1, maxcF_out_ga(X1, X2)) → U25_GA(X1, delcG_in_gga(X2, X1)) at position [1] we obtained the following new rules [LPAR04]:

U24_GA(x0, maxcF_out_ga(x0, f)) → U25_GA(x0, delcG_out_gga(f, x0, .(f, x0)))

(87) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U25_GA(X1, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(f, X1))) → U24_GA(X1, maxcF_in_ga(X1))
U24_GA(x0, maxcF_out_ga(x0, f)) → U25_GA(x0, delcG_out_gga(f, x0, .(f, x0)))

The TRS R consists of the following rules:

delcG_in_gga(f, X1) → delcG_out_gga(f, X1, .(f, X1))
maxcF_in_ga([]) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1)) → U51_ga(X1, maxcF_in_ga(X1))
maxcF_in_ga(.(t, X1)) → U52_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga([]) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1)) → U48_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga(.(f, X1)) → U49_ga(X1, maxcC_in_ga(X1))
U52_ga(X1, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U49_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
U51_ga(X1, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)

The set Q consists of the following terms:

maxcC_in_ga(x0)
maxcF_in_ga(x0)
delcG_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)

We have to consider all (P,Q,R)-chains.

(88) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(89) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U25_GA(X1, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(f, X1))) → U24_GA(X1, maxcF_in_ga(X1))
U24_GA(x0, maxcF_out_ga(x0, f)) → U25_GA(x0, delcG_out_gga(f, x0, .(f, x0)))

The TRS R consists of the following rules:

maxcF_in_ga([]) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1)) → U51_ga(X1, maxcF_in_ga(X1))
maxcF_in_ga(.(t, X1)) → U52_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga([]) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1)) → U48_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga(.(f, X1)) → U49_ga(X1, maxcC_in_ga(X1))
U52_ga(X1, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U49_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
U51_ga(X1, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)

The set Q consists of the following terms:

maxcC_in_ga(x0)
maxcF_in_ga(x0)
delcG_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)

We have to consider all (P,Q,R)-chains.

(90) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

delcG_in_gga(x0, x1)

(91) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U25_GA(X1, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(f, X1))) → U24_GA(X1, maxcF_in_ga(X1))
U24_GA(x0, maxcF_out_ga(x0, f)) → U25_GA(x0, delcG_out_gga(f, x0, .(f, x0)))

The TRS R consists of the following rules:

maxcF_in_ga([]) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1)) → U51_ga(X1, maxcF_in_ga(X1))
maxcF_in_ga(.(t, X1)) → U52_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga([]) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1)) → U48_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga(.(f, X1)) → U49_ga(X1, maxcC_in_ga(X1))
U52_ga(X1, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U49_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
U51_ga(X1, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)

The set Q consists of the following terms:

maxcC_in_ga(x0)
maxcF_in_ga(x0)
U48_ga(x0, x1)
U49_ga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)

We have to consider all (P,Q,R)-chains.

(92) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U25_GA(X1, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4) we obtained the following new rules [LPAR04]:

U25_GA(z0, delcG_out_gga(f, z0, .(f, z0))) → MAXSORTA_IN_GA(.(f, z0))

(93) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MAXSORTA_IN_GA(.(f, .(f, X1))) → U24_GA(X1, maxcF_in_ga(X1))
U24_GA(x0, maxcF_out_ga(x0, f)) → U25_GA(x0, delcG_out_gga(f, x0, .(f, x0)))
U25_GA(z0, delcG_out_gga(f, z0, .(f, z0))) → MAXSORTA_IN_GA(.(f, z0))

The TRS R consists of the following rules:

maxcF_in_ga([]) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1)) → U51_ga(X1, maxcF_in_ga(X1))
maxcF_in_ga(.(t, X1)) → U52_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga([]) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1)) → U48_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga(.(f, X1)) → U49_ga(X1, maxcC_in_ga(X1))
U52_ga(X1, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U49_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
U51_ga(X1, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)

The set Q consists of the following terms:

maxcC_in_ga(x0)
maxcF_in_ga(x0)
U48_ga(x0, x1)
U49_ga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)

We have to consider all (P,Q,R)-chains.

(94) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

MAXSORTA_IN_GA(.(f, .(f, X1))) → U24_GA(X1, maxcF_in_ga(X1))
U24_GA(x0, maxcF_out_ga(x0, f)) → U25_GA(x0, delcG_out_gga(f, x0, .(f, x0)))
U25_GA(z0, delcG_out_gga(f, z0, .(f, z0))) → MAXSORTA_IN_GA(.(f, z0))


Used ordering: Polynomial interpretation [POLO]:

POL(.(x1, x2)) = 1 + 2·x1 + 2·x2   
POL(MAXSORTA_IN_GA(x1)) = 2·x1   
POL(U24_GA(x1, x2)) = 1 + x1 + 2·x2   
POL(U25_GA(x1, x2)) = 2 + x1 + x2   
POL(U48_ga(x1, x2)) = 1 + x1 + x2   
POL(U49_ga(x1, x2)) = 1 + x1 + x2   
POL(U51_ga(x1, x2)) = 2 + 2·x1 + x2   
POL(U52_ga(x1, x2)) = 2 + 2·x1 + 2·x2   
POL([]) = 0   
POL(delcG_out_gga(x1, x2, x3)) = x1 + 2·x2 + x3   
POL(f) = 0   
POL(maxcC_in_ga(x1)) = 1 + x1   
POL(maxcC_out_ga(x1, x2)) = 1 + x1 + 2·x2   
POL(maxcF_in_ga(x1)) = 2 + 2·x1   
POL(maxcF_out_ga(x1, x2)) = 2 + 2·x1 + 2·x2   
POL(t) = 0   

(95) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

maxcF_in_ga([]) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1)) → U51_ga(X1, maxcF_in_ga(X1))
maxcF_in_ga(.(t, X1)) → U52_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga([]) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1)) → U48_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga(.(f, X1)) → U49_ga(X1, maxcC_in_ga(X1))
U52_ga(X1, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U49_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
U51_ga(X1, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)

The set Q consists of the following terms:

maxcC_in_ga(x0)
maxcF_in_ga(x0)
U48_ga(x0, x1)
U49_ga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)

We have to consider all (P,Q,R)-chains.

(96) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(97) YES